proposition: Lemma sum_vector_assoc: forall (dim:nat) (v1 v2 v3: vector dim), sum_vector _ (sum_vector _ v1 v2) v3 ==v sum_vector _ v1 (sum_vector _ v2 v3).
proof: Proof. fix sum_vector_assoc 1. intros [|dim]. simpl. intros v1 v2 v3. apply plus_assoc. simpl. intros [c1 v1] [c2 v2] [c3 v3]. split. apply plus_assoc. apply sum_vector_assoc. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)