From 31deebd19b46df40b2503f65f687ea6a5aeb7e42 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Sun, 24 Nov 2024 12:44:35 -0500 Subject: [PATCH] feat: `Nat.lt_pow_self` --- src/Init/Data/Nat/Lemmas.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index cb60267c5d60..c9bcfccc6256 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -846,6 +846,18 @@ protected theorem pow_lt_pow_iff_pow_mul_le_pow {a n m : Nat} (h : 1 < a) : rw [←Nat.pow_add_one, Nat.pow_le_pow_iff_right (by omega), Nat.pow_lt_pow_iff_right (by omega)] omega +protected theorem lt_pow_self {n a : Nat} (h : 1 < a) : n < a ^ n := by + induction n with + | zero => exact Nat.zero_lt_one + | succ _ ih => exact Nat.lt_of_lt_of_le (Nat.add_lt_add_right ih 1) (Nat.pow_lt_pow_succ h) + +protected theorem lt_two_pow : n < 2 ^ n := + Nat.lt_pow_self Nat.one_lt_two + +@[simp] +protected theorem mod_two_pow : n % 2 ^ n = n := + Nat.mod_eq_of_lt Nat.lt_two_pow + @[simp] theorem two_pow_pred_mul_two (h : 0 < w) : 2 ^ (w - 1) * 2 = 2 ^ w := by