proposition: Lemma valid_sep3 (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. apply/idP/idP. - move=>W; case/valid_sepI/andP: (W). rewrite pfjoin ?(validL W) // =>->-> /=. by rewrite andbT; case/validL/valid_sepI/andP: W. case/and3P=>W D1 D2; rewrite valid_sep pfjoin ?W ?D2 //. by rewrite valid_sep (validL W) D1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)