proposition: Lemma lfpE : lfp = F lfp.
proof: Proof. Proof using monoF. suff: exists k : 'I_#|T|.+1 , iter k F set0 == iter k.+1 F set0. case => k /eqP E. apply: iter_fix E _. exact: leq_ord. apply/existsP. rewrite -[[exists _,_]]negbK negb_exists. apply/negP => /forallP => H. have/(_ #|T|.+1 (leqnn _)): forall k , k <= #|T|.+1 -> k <= #|iter k F set0|. elim => // n IHn Hn. apply: leq_ltn_trans (IHn (ltnW Hn)) _. apply: proper_card. rewrite properEneq iterFsub andbT. exact: (H (Ordinal Hn)). apply/negP. rewrite leqNgt negbK. by rewrite ltnS max_card. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)