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