proposition: Lemma prec_flip x1 x2 y1 y2 : valid (x1 \+ y1) -> x1 \+ y1 = x2 \+ y2 -> valid (y2 \+ x2) /\ y2 \+ x2 = y1 \+ x1.
proof: Proof. by move=>X /esym E; rewrite joinC E X joinC. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)