proposition: Lemma tarski_lfp_mono (f1 f2 : T -> T) : monotone f2 -> f1 <== f2 -> tarski_lfp f1 <== tarski_lfp f2.
proof: Proof. move=>M H; apply/infP/(poset_trans (H (tarski_lfp f2))). by rewrite tarski_lfp_fixed. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude)