proposition: Lemma nv_nullify_prc_left : forall dim c, prod_row_col _ (null_vector dim) c == rO.
proof: Proof. induction dim. vm_compute;intros. ring. simpl. intros [a v]. rewrite IHdim. ring. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)