proposition: Lemma finset_gt_wf: well_founded (fun x y => finset_le y x /\ ~finset_eq y x).
proof: Proof. set (M := fun x => (IdentSet.cardinal U - finset_cardinal x)%nat). apply wf_incl with (ltof _ M). - red; intros x y [L E]; red. unfold M. generalize (finset_cardinal_max x), (finset_cardinal_max y), (finset_cardinal_lt y x L E); intros. lia. - apply well_founded_ltof. Qed.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation) CDF(Fixpoints)