proposition: Fact vec_sum_plus n v w : @vec_sum n (vec_plus v w) = vec_sum v + vec_sum w.
proof: Proof. revert w; induction v; intros w. 1: rewrite (vec_0_nil (vec_plus _ _)), (vec_0_nil w); auto. rewrite (vec_head_tail w), vec_plus_cons; simpl. rewrite IHv; lia. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)