proposition: Lemma choose_step_acc : (∃ x, P x) → Acc choose_step 1%positive.
proof: Proof. intros [x Hx]. cut (∀ i p, i ≤ encode x → 1 + encode x = p + i → Acc choose_step p). { intros help. by apply (help (encode x)). } intros i. induction i as [|i IH] using Pos.peano_ind; intros p ??. { constructor. intros j. assert (p = encode x) by lia; subst. inv 1 as [? Hd|?? Hd]; rewrite decode_encode in Hd; congruence. } constructor. intros j. inv 1 as [? Hd|? y Hd]; auto with lia. Qed.
imports: Coq.QArith(QArith_base Qcanon) stdpp(well_founded) stdpp(options)