proposition: Lemma valid_sep3I (x y z : U) : valid (x \+ y \+ z) -> [&& valid (pval x \+ pval y \+ pval z), D (pval x) (pval y) & D (pval x \+ pval y) (pval z)].
proof: Proof. by rewrite valid_sep3. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)