proposition: Fact pow2_2n1_dec n : { p : nat & { b | S n = pow2 p*(2*b+1) } }.
proof: Proof. induction on n as IH with measure n. generalize (div2_spec (S n)). destruct (div2 (S n)) as (d,[]); intros Hn. + exists 0, d; simpl; lia. + destruct d as [ | d ]. * simpl in Hn; lia. * destruct (IH d) as (p & b & H). - lia. - exists (S p), b; rewrite pow2_fix1, <- Nat.mul_assoc, <- H; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)