proposition: Lemma freshfUnT U D (f : @morphism U (nat_mapPCM A) D) fr : forall x y : U, valid (x \+ y) -> D x y -> fresh (f (x \+ y)) <= fr -> fresh (f x) <= fr.
proof: Proof. move=>x y V H; apply: leq_trans. by rewrite pfjoin // freshfUn // pfV2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval) pcm(options prelude pred finmap rtc seqext useqord uslice uconsec)