proposition: Lemma kleene_lfp_least : forall x, f x = x -> kleene_lfp <== x.
proof: Proof. move=>x H; apply: limM=>y [n][->] _. by elim: n=>[|n IH] //=; rewrite -H; apply: cont_mono IH. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)