proposition: Lemma rI_neutral_psv : forall dim v, prod_scal_vec dim rI v ==v v.
proof: Proof. induction dim. intros; vm_compute;ring. unfold null_vector in *;simpl;intros [a v]. rewrite IHdim. split;try ring. reflexivity. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)