proposition: Lemma fix_mono (f1 f2 : lat -> lat) : f1 <== f2 -> (Fix f1 : lat) <== Fix f2.
proof: Proof. move=>Hf; apply: tarski_lfp_mono. - move=>x1 x2 Hx; apply: supM=>z [x][H ->]; apply: supP; exists x. by split=>//; apply: poset_trans H Hx. move=>y; apply: supM=>_ [x][H1 ->]. by apply: poset_trans (Hf x) _; apply: supP; exists x. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)