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