proposition: Lemma mxE3 t x : ((((mx t \+ x == nown) = false) * ((x \+ mx t == nown) = false)) * (((nown == mx t \+ x) = false) * ((nown == x \+ mx t) = false))).
proof: Proof. by case: x. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options prelude pred) pcm(pcm morphism natmap)