proposition: Lemma xsep_joinAC : right_commutative xsep_join.
proof: Proof. case=>a Ha [b Hb][c Hc]; apply: xval_inj; rewrite /= /xsep_join !unlock /xsep_join' /=. case Sab: (orth2 a b); case Sac: (orth2 a c); rewrite ?tpcmE //=; last first. - case/andP: Sac=>_ Sac; case: andP=>//; case=>W Sacb. by rewrite (sepAxx W Sac Sacb) andbT (validLE3 W) in Sab. - case/andP: Sab=>_ Sab; case: andP=>//; case=>W Sabc. by rewrite (sepAxx W Sab Sabc) andbT (validLE3 W) in Sac. case/andP: Sab=>_ Sab; case/andP: Sac=>_ Sac. case Sabc: (orth2 (a \+ b) c). - case/andP: Sabc=>W Sabc; rewrite sepC (joinAC a c b) W //. by rewrite (sepAxx W Sab Sabc). case Sacb: (orth2 (a \+ c) b)=>//. case/andP: Sacb=>W Sacb; rewrite sepC (joinAC a b c) W // in Sabc. by rewrite (sepAxx W Sac Sacb) in Sabc. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(eqtype fintype) pcm(options axioms prelude) pcm(pcm)