English
For a natural number n and x ∈ PartENat, (n : PartENat) < x iff for all h ∈ x.Dom, n < x.get(h).
Русский
Для натурального n и x ∈ PartENat, (n : PartENat) < x тогда и только тогда, когда для всех h ∈ x.Dom выполняется n < x.get(h).
LaTeX
$$$ (n : \mathrm{PartENat}) < x \iff \\forall h : x.Dom, n < x.get(h) $$$
Lean4
theorem lt_coe_iff (x : PartENat) (n : ℕ) : x < n ↔ ∃ h : x.Dom, x.get h < n := by
simp only [lt_def, forall_prop_of_true, get_natCast', dom_natCast]