proposition: Lemma zero_matrix_mult_l : forall m n p (M : matrix n p), zero_matrix m n <*> M =m zero_matrix m p.
proof: Proof. unfold mat_eqA. intros. unfold zero_matrix at 2. mat_get_simpl. fold (get_row (zero_matrix m n <*> M) ip). fold (get_elem (zero_matrix m n <*> M) ip jp). rewrite mat_mult_spec, dot_product_zero, mat_build_nth. refl. apply Vforall_nth_intro. intros. unfold zero_matrix. mat_get_simpl. rewrite mat_build_nth. refl. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)