proposition: Lemma perm_mx1 : forall n, perm_mx 1 === @scalar_mx n 1.
proof: Proof. by move=> n i j; rewrite /perm_mx /scalar_mx perm1; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms