proposition: Lemma finset_cardinal_lt: forall x y, finset_le x y -> ~finset_eq x y -> (finset_cardinal x < finset_cardinal y)%nat.
proof: Proof. intros. destruct (IdentSet.choose (IdentSet.diff (proj1_sig y) (proj1_sig x))) as [elt|] eqn:CHOOSE. - apply IdentSet.choose_1 in CHOOSE. apply ISProp.subset_cardinal_lt with elt. auto. fsetdec. fsetdec. - apply IdentSet.choose_2 in CHOOSE. assert (finset_le y x). { intros e IN. destruct (ISProp.In_dec e (proj1_sig x)); auto. elim (CHOOSE e). apply IdentSet.diff_3; auto. } elim H0. apply ISProp.subset_antisym; auto. Qed.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation) CDF(Fixpoints)