proposition: Lemma tarski_lfp_fixed (f : T -> T) : monotone f -> f (tarski_lfp f) = tarski_lfp f.
proof: Proof. move=>M; suff L: f (tarski_lfp f) <== tarski_lfp f. - by apply: poset_asym=>//; apply: infP; apply: M L. by apply: infM=>x L; apply: poset_trans (L); apply: M; apply: infP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)