diff --git a/library/data/pnat.lean b/library/data/pnat.lean index 7cff0416d..69131888c 100644 --- a/library/data/pnat.lean +++ b/library/data/pnat.lean @@ -325,5 +325,7 @@ theorem p_add_fractions (n : ℕ+) : (2 * n)⁻¹ + (2 * 3 * n)⁻¹ + (3 * n) assert T : 2⁻¹ + 2⁻¹ * 3⁻¹ + 3⁻¹ = 1, from dec_trivial, by rewrite[*inv_mul_eq_mul_inv,-*rat.right_distrib,T,rat.one_mul] +theorem rat_power_two_le (k : ℕ+) : rat_of_pnat k ≤ rat.pow 2 k~ := + !binary_nat_bound end pnat diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean index 2f22b7ca6..0d534ca71 100644 --- a/library/data/rat/order.lean +++ b/library/data/rat/order.lean @@ -449,4 +449,19 @@ calc theorem ubound_pos (a : ℚ) : nat.gt (ubound a) nat.zero := !nat.succ_pos +theorem binary_nat_bound (a : ℕ) : of_nat a ≤ pow 2 a := + nat.induction_on a (zero_le_one) + (take n, assume Hn, + calc + of_nat (nat.succ n) = (of_nat n) + 1 : of_nat_add + ... ≤ pow 2 n + 1 : add_le_add_right Hn + ... ≤ pow 2 n + rat.pow 2 n : + add_le_add_left (pow_ge_one_of_ge_one two_ge_one _) + ... = pow 2 (nat.succ n) : pow_two_add) + +theorem binary_bound (a : ℚ) : ∃ n : ℕ, a ≤ pow 2 n := + exists.intro (ubound a) (calc + a ≤ of_nat (ubound a) : ubound_ge + ... ≤ pow 2 (ubound a) : binary_nat_bound) + end rat