proposition: Lemma level2 (x y : T) (lx : x \in lfp) : y \in iter (levl lx) F fset0 -> exists ly, @levl y ly < levl lx.
proof: Proof. move => iter_y. have ly : y \in lfp. move: iter_y. apply: (subP (iterFsub _)). apply: ltnW. exact: level_max. exists ly. rewrite {1}/levl. case: (ex_minnP _) => m m1 m2. move: iter_y. case e: (levl lx) => [|n]; first by rewrite /= inE. exact: m2. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)