proposition: Lemma card_of_list_eq_length_gen l (h : finite (of_list l)) : nodup l -> card h = length l.
proof: Proof. intro l_nodup. destruct (dec (l = nil)) as [hl|hl]. subst. rewrite card_empty_gen. refl. assert (a : A). destruct l. cong. exact a. apply Nat.le_antisymm. apply card_of_list_le_length_gen. 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]]]. apply N_inj_le with (f := fun x : N (length l) => inverse f_surj (elt (P:=of_list l) (nth_In a x))). intros [x_val x] [y_val y] e. apply N_eq; simpl. apply inj_inverse in e. apply sig_eq in e; simpl in e. apply inj_nth_nodup in e; auto. apply eq_dec. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)