proposition: Theorem log2_power: forall n, 0 < n -> ( exp2 (log2 n) <= n < 2 * exp2 (log2 n) ).
proof: Proof. intros n; elim n using (well_founded_ind lt_wf). intros x; case x. - simpl; intros; lia. - intros x'; case x'. + rewrite (log2_fix_eqn 1); simpl; auto with arith. + intros p Hrec; elim (Hrec (div2 (S (S p)))). * intros Hle Hlt _; rewrite (log2_fix_eqn (S (S p))). cbv zeta iota beta delta [exp2]; fold exp2. split. apply Nat.le_trans with (2 * div2 (S (S p))). auto with arith. elim (div2_eq (S (S p))). lia. lia. apply Nat.le_lt_trans with (2 * div2 (S (S p)) + 1). elim (div2_eq (S (S p))). lia. lia. lia. * apply div2_lt; simpl; auto with arith. * simpl; auto with arith. Qed.
imports: Arith ArithRing Lia Wf_nat