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