proposition: Lemma pfjoinV x y : valid (x \+ y) -> D x y -> valid (f x \+ f y) /\ f (x \+ y) = f x \+ f y.
proof: Proof. by case: f=>g [H1 H2]; apply: H2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)