proposition: Lemma orthXEQ (U : pcm) (D1 D2 : rel U) : D1 =2 D2 -> orth_axiom D1 <-> orth_axiom D2.
proof: Proof. move=>H; split; case=>H1 H2 H3 H4 H5. - by split=>[|x y|x y|x y|x y z]; rewrite -!H; [apply: H1 | apply: H2 | apply: H3 | apply: H4 | apply: H5]. by split=>[|x y|x y|x y|x y z]; rewrite !H; [apply: H1 | apply: H2 | apply: H3 | apply: H4 | apply: H5]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)