proposition: Lemma xorth_gsep : xgseprel_axiom -> seprel_axiom (fun x y => nsep x y && nsep y x).
proof: Proof. case=>H1 Xp Xq1 Xq2 H2 H3 H4 H5 H6; apply: orth_nsep. split=>[|x y V|y V|x y z V|x y z V]. - by apply/pf1. - by move/pf1=>H; apply/pf1=>k /[dup] Y /H; apply: H3 V Y. - by apply/pf1=>x; apply: H4. - have V' : valid (x \+ y) by rewrite (validLE3 V). move/pf1=>X1 /pf1 X2; apply/pf1=>k Hx; apply: (H5)=>//; last first. - by apply: X2; apply/H1=>//; left. - by apply: X1. move=>k' Hy; apply: Xp (V') (Hx) (Hy) _. have Hxy : P k' (x \+ y) by rewrite H1 //; right. by apply: Xq1 V (Hx) (X1 _ Hx) (X2 _ Hxy). have V' : valid (x \+ y) by rewrite (validLE3 V). move/pf1=>X1 /pf1 X2; split; apply/pf1=>k Hx. - case: (H6 k x y z V Hx)=>//; last by apply: X1. move=>k' Hy; apply: Xp V' (Hx) (Hy) _. by apply: Xq2 (X1 _ Hx) _ (X2 _ Hy). case/H1: Hx; first by rewrite (validLE3 V). - move=>Hx; case: (H6 k x y z V Hx)=>//; last by apply: X1. by move=>k' Hy; apply: Xp V' (Hx) (Hy) _; apply: Xq2 (X1 _ Hx) _ (X2 _ Hy). move=>Hy; rewrite joinC. case: (H6 k y x z)=>//; first by rewrite (validLE3 V). - by move=>k' Hx; apply: Xp V' (Hx) (Hy) _; apply: Xq2 (X1 _ Hx) _ (X2 _ Hy). by apply: X2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)