a_add_one_le_four_pow_parts_card — Mathlib

English

There is an inequality a + 1 ≤ 4^{#P.parts}.

Русский

Существует неравенство a+1 ≤ 4^{#P.parts}.

LaTeX

$$a + 1 ≤ 4^{#P.parts}$$

Lean4

theorem a_add_one_le_four_pow_parts_card : a + 1 ≤ 4 ^ #P.parts :=
  by
  have h : 1 ≤ 4 ^ #P.parts := one_le_pow₀ (by simp)
  rw [stepBound, ← Nat.div_div_eq_div_mul]
  conv_rhs => rw [← Nat.sub_add_cancel h]
  rw [add_le_add_iff_right, tsub_le_iff_left, ← Nat.add_sub_assoc h]
  exact Nat.le_sub_one_of_lt (Nat.lt_div_mul_add h)

Похожие утверждения