proposition: Lemma rO_nullify_psv : forall dim v, prod_scal_vec _ rO v ==v null_vector dim .
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)