proposition: Lemma trmxK : forall m n, setoid_cancel (@trmx m n) (@trmx n m).
proof: Proof. by move=> m n A i j; rewrite/trmx; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms