proposition: Lemma nv_neutral_right_sv : forall dim v, sum_vector dim v (null_vector dim) ==v v.
proof: Proof. induction dim. simpl. unfold null_vector. simpl. intros;ring. simpl. intros [a v]. split;try ring. apply IHdim. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)