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