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