proposition: Lemma f'_mono : monotone f'.
proof: Proof. move=>x y H; apply: sup_mono=>fz; case=>z [Hz {fz}->]. by exists z; split=>//; apply/poset_trans/H. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun ssrnat eqtype seq) pcm(options axioms pred prelude) pcm(pcm unionmap heap) htt(domain)