proposition: Lemma sum_vector_comm: forall (dim:nat) (v1 v2: vector dim), sum_vector _ v1 v2 ==v sum_vector _ v2 v1.
proof: Proof. apply sum_vector_comm with (eq:=eq) (plus:=plus). intros;ring. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)