proposition: Lemma nm_nullify_psm : forall dim a, prod_scal_mat _ a (null_matrix _) ==m null_matrix dim .
proof: Proof. induction dim. intros; vm_compute;ring. unfold null_matrix in *;simpl;intros a. rewrite IHdim. repeat split;try ring. apply nv_nullify_psv. apply nv_nullify_psv. reflexivity. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)