proposition: Fact vec_add_assoc u v w : vec_plus u (vec_plus v w) = vec_plus (vec_plus u v) w.
proof: Proof. apply vec_pos_ext. intros p; unfold vec_zero, vec_plus. repeat rewrite vec_pos_set; lia. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)