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