Removing lemmas

theories/VLSM/Lib/FinExtras.v

@@ -11,13 +11,6 @@ Fixpoint up_to_n_listing
   | S n' => n' :: up_to_n_listing n'
   end.
 
-Lemma up_to_n_listing_length
-  (n : nat)
-  : length (up_to_n_listing n) = n.
-Proof.
-  induction n; simpl; congruence.
-Qed.
-
 Lemma up_to_n_full
   (n : nat)
   : forall i, i < n <-> i ∈ up_to_n_listing n.

theories/VLSM/Lib/FinFunExtras.v

@@ -68,13 +68,4 @@ Proof.
   by destruct a;simpl;congruence.
 Qed.
 
-Lemma right_finite
-  (sum_finite : Listing sum_listing)
-  : Listing (right_listing sum_finite).
-Proof.
-  revert sum_finite.
-  apply map_option_listing with (g:=inr); [| done].
-  by destruct a;simpl;congruence.
-Qed.
-
 End sum_listing.