proposition: Lemma rI_neutral_psm : forall dim m, prod_scal_mat dim rI m ==m m.
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 rI_neutral_psv. apply rI_neutral_psv. reflexivity. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)