English
For any natural number n and x ∈ PartENat, (n : PartENat) < x iff ∀ 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 coe_lt_iff (n : ℕ) (x : PartENat) : (n : PartENat) < x ↔ ∀ h : x.Dom, n < x.get h :=
by
rw [← some_eq_natCast]
simp only [lt_def, exists_prop_of_true, dom_some]
rfl