proposition: Lemma orth_nsep (U : pcm) (nsep : rel U) : nseprel_axiom nsep -> seprel_axiom (fun x y => nsep x y && nsep y x).
proof: Proof. case=>H1 H2 H3 H4 H5; split=>[|x y V|x y V|x y z V]. - by rewrite H1. - by rewrite andbC. - by case/andP=>/(H2 _ _ V) -> _; rewrite (H3 _ (validL V)). case/andP=>X1 X2 /andP [X3 X4]. move: (H4 x y z V X1 X3)=>X5; rewrite X5 /=. rewrite joinC in X3. move: (H4 y x z); rewrite (validLE3 V)=>/(_ erefl X2 X3) X6. rewrite joinC in X4; rewrite joinC in X6. move: (H5 y z x); rewrite (validLE3 V)=>/(_ erefl X6 X4) [->->] /=. by move: (H5 z y x); rewrite (validLE3 V)=>/(_ erefl X4 X6) [] ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)