proposition: Lemma orth_sep (U : pcm) (sep : rel U) : seprel_axiom sep <-> orth_axiom (fun x y => valid (x \+ y) && sep x y).
proof: Proof. split. - case=>H1 H2 H3 H4; split=>[|x y|x y|x y|x y z]. - by rewrite unitL valid_unit H1. - by apply/andP/andP; case=> V; rewrite H2 (validE2 V). - by case/andP. - by case/andP=> V S; rewrite unitR (H3 x y) ?(validE2 V). case/andP=>_ S1 /andP [V2 S2]. by rewrite !(andX (H4 _ _ _ V2 S1 S2)) !(validLE3 V2). case=>H1 H2 H3 H4 H5; split=>[|x y V|x y V S|x y z V H S]. - by case/andP: H1. - by move: (H2 x y); rewrite !(validE2 V). - by rewrite (andX (H4 x y _)) // V S. by move: (@H5 x y z); rewrite !(validLE3 V) H S => /(_ erefl erefl). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)