proposition: Lemma nv_nullify_prm : forall dim m, prod_row_mat _ (null_vector _) m ==v null_vector dim .
proof: Proof. induction dim. intros; vm_compute;ring. unfold null_matrix,null_vector in *;simpl;intros [a [r [c m]]]. rewrite IHdim. repeat split. rewrite nv_nullify_prc_left. ring. rewrite rO_nullify_psv. rewrite nv_neutral_left_sv. reflexivity. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)