proposition: Theorem vec_nat_induction v : P v.
proof: Proof. Proof using HP0 HP1 HP2. induction v as [ v IHv ] using (measure_rect (@vec_sum n)). case_eq (vec_sum v). + intros Hv; apply vec_sum_is_zero in Hv; subst; auto. + intros x Hx. destruct (vec_sum_is_nzero v) as (p & w & Hw). * lia. * subst. apply HP2; auto. apply IHv. rewrite vec_sum_plus, vec_sum_one; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)