proposition: Fact vec_plus_is_zero u v : vec_zero = vec_plus u v -> u = vec_zero /\ v = vec_zero.
proof: Proof. unfold vec_zero, vec_plus; intros H; split; apply vec_pos_ext; intros p; apply f_equal with (f := fun v => vec_pos v p) in H; repeat rewrite vec_pos_set in * |- *; lia. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)