feat: Nat.lt_pow_self (leanprover#6200)

This PR upstreams `Nat.lt_pow_self` and `Nat.lt_two_pow` from Mathlib
and uses them to prove the simp theorem `Nat.mod_two_pow`.

This simplifies expressions like `System.Platform.numBits % 2 ^
System.Platform.numBits = System.Platform.numBits`, which is needed for
leanprover#6188.

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_self : n < 2 ^ n :=
+  Nat.lt_pow_self Nat.one_lt_two
+
+@[simp]
+protected theorem mod_two_pow_self : n % 2 ^ n = n :=
+  Nat.mod_eq_of_lt Nat.lt_two_pow_self
+
 @[simp]
 theorem two_pow_pred_mul_two (h : 0 < w) :
     2 ^ (w - 1) * 2 = 2 ^ w := by