proposition: Lemma tarski_lfp_least f : forall x : T, f x = x -> tarski_lfp f <== x.
proof: Proof. by move=>x H; apply: infP; rewrite InE /= H. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)