proposition: Fact vec_sum_is_nzero n v : 0 < @vec_sum n v -> { p : _ & { w | v = vec_plus (vec_one p) w } }.
proof: Proof. induction v as [ | [ | x] n v IHv ]; intros Hv; simpl in Hv. + lia. + apply IHv in Hv. destruct Hv as (p & w & Hw). exists (pos_nxt p), (0##w); rewrite vec_one_nxt. rewrite vec_plus_cons; f_equal; auto. + exists pos0, (x##v). rewrite vec_one_fst, vec_plus_cons; rew vec. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)