proposition: Lemma id_matrix_neutral_right_pm : forall dim m, prod_matrix dim m (id_matrix dim) ==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_right);ring. rewrite nv_nullify_psv. rewrite nv_neutral_left_sv. rewrite im_neutral_prm. reflexivity. rewrite nv_nullify_pmc. rewrite nv_neutral_right_sv. rewrite rI_neutral_psv. reflexivity. rewrite nv_nullify_pcr_right. rewrite nm_neutral_left_sum_matrix. apply IHdim. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)