proposition: Lemma mxyMx t x y : valid (y \+ mx t \+ x) -> y \+ x = Unit.
proof: Proof. by rewrite joinAC=>/mxMx. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)