proposition: Lemma mat_mult_id_l : forall n p (np : n >= p) (M : matrix n p), id_matrix n <*> M =m M.
proof: Proof. unfold mat_eqA. intros. rewrite mat_mult_spec. unfold id_matrix, get_row. rewrite Vbuild_nth, (dot_product_id ip). mat_get_simpl. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)