proposition: Lemma lfpE : lfp = F lfp.
proof: Proof. Proof using F_bound F_mono. suff: exists k : 'I_(size U).+1 , iter k F fset0 == iter k.+1 F fset0. case => k /eqP E. apply: iter_fix E _. exact: leq_ord. apply/existsP. apply: contraT. rewrite negb_exists => /forallP H. have: forall k , k <= (size U).+1 -> k <= size (iter k F fset0). elim => // n IHn Hn. apply: leq_ltn_trans (IHn (ltnW Hn)) _. apply: proper_size. rewrite properEneq iterFsub1 andbT. exact: (H (Ordinal Hn)). move/(_ (size U).+1 (leqnn _)). rewrite leqNgt ltnS subset_size //. exact: iterFbound. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)