proposition: Lemma id_matrix_neutral_left_pm : forall dim m, prod_matrix dim (id_matrix dim) m ==m m.
proof: Proof. induction dim. simpl. unfold null_matrix. simpl. intros;ring. simpl. intros [a [r [c m]]]. repeat split. rewrite (nv_nullify_prc_left);ring. rewrite rI_neutral_psv. rewrite nv_nullify_prm. rewrite nv_neutral_right_sv. reflexivity. rewrite nv_nullify_psv. rewrite nv_neutral_left_sv. rewrite im_neutral_pmc. reflexivity. rewrite nv_nullify_pcr_left. rewrite nm_neutral_left_sum_matrix. apply IHdim. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)