proposition: Lemma nv_nullify_pmc : forall dim m, prod_mat_col _ m (null_vector _) ==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_right. 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)