proposition: Fact vec_sum_one n p : @vec_sum n (vec_one p) = 1.
proof: Proof. revert p; induction n as [ | n IHn ]; intros p. 1: invert pos p. pos_inv p. + rewrite vec_one_fst. simpl; f_equal; apply vec_sum_zero. + rewrite vec_one_nxt. unfold vec_sum; fold vec_sum. rewrite IHn; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)