unpair_lt — Mathlib

English

If n ≥ 1, then the first component of unpair(n) is strictly less than n.

Русский

Если n ≥ 1, то первая компонента распаковки меньше n.

LaTeX

$$$ \forall n \in \mathbb{N}, \; 1 \le n \Rightarrow \operatorname{fst}(\operatorname{unpair}(n)) < n. $$$

Lean4

theorem unpair_lt {n : ℕ} (n1 : 1 ≤ n) : (unpair n).1 < n :=
  by
  let s := sqrt n
  simp only [unpair]
  by_cases h : n - s * s < s <;> simp only [h, ↓reduceIte, gt_iff_lt, s]
  · exact lt_of_lt_of_le h (sqrt_le_self _)
  · simp only [not_lt] at h
    have s0 : 0 < s := sqrt_pos.2 n1
    exact lt_of_le_of_lt h (Nat.sub_lt n1 (Nat.mul_pos s0 s0))

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