proposition: Lemma card_of_list_le_length_gen l (h : finite (of_list l)) : card h <= length l.
proof: Proof. unfold card. case_eq (mk_Pf h); intros P P_fin e; apply sig_eq in e; simpl in e; subst. destruct (cdd (card_uniq P_fin)) as [n [f [f_inj f_surj]]]. destruct n. lia. set (g := fun i : N (S n) => let (_, xl) := f i in N_ (pos_lt_length eq_dec xl)). apply N_inj_le with (f := g). intros i j. unfold g. case_eq (f i); intros x xl hx. case_eq (f j); intros y yl hy e. apply N_eq in e; simpl in e. apply inj_pos in e. 2: fo. subst y. apply f_inj. rewrite hx, hy. apply sig_eq. refl. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)