proposition: Lemma orth_gsep : gseprel_axiom -> seprel_axiom (fun x y => nsep x y && nsep y x).
proof: Proof. case=>H1 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. - move/pf1=>X1 /pf1 X2; apply/pf1=>k H. apply: H5=>//; first by apply: X1 H. by apply: X2; apply/H1; [rewrite (validLE3 V)|left]. move/pf1=>X1 /pf1 X2; split; apply/pf1=>k H. - by case: (H6 k x y z V H (X1 _ H)). case/H1: H; first by rewrite (validLE3 V). - by move=>H; case: (H6 k x y z V H (X1 _ H)). move=>H; rewrite joinC. case: (H6 k y x z)=>//; first by rewrite (validLE3 V). by apply: X2 H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)