proposition: Lemma mulmx1 : forall m n (A : 'M_(m, n)), A *m 1%:M === A.
proof: Proof. move=> m n A i k; rewrite/mulmx/scalar_mx. setoid_rewrite (bigD1 (j:=k))=>//. setoid_rewrite big1=> [| j/=]; first by rewrite eq_refl; ring. by rewrite/is_true; move/negbRL=>->/=; ring. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms