proposition: Lemma mulmx0 : forall m n p (A : 'M_(m, n)), A *m '0m === @null_mx m p.
proof: Proof. by move=> m n p A i k; rewrite/mulmx/null_mx; apply (big1 (P:=fun _ => true) (F:=fun j => A i j * 0))=> j _; ring. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms