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