feat(set_theory/ordinal_arithmetic): le_one_iff (#11847)

src/set_theory/ordinal_arithmetic.lean

@@ -183,6 +183,15 @@ instance : nontrivial ordinal.{u} :=
 theorem zero_lt_one : (0 : ordinal) < 1 :=
 lt_iff_le_and_ne.2 ⟨ordinal.zero_le _, ne.symm $ ordinal.one_ne_zero⟩
 
+theorem le_one_iff {a : ordinal} : a ≤ 1 ↔ a = 0 ∨ a = 1 :=
+begin
+  refine ⟨λ ha, _, _⟩,
+  { rcases eq_or_lt_of_le ha with rfl | ha,
+    exacts [or.inr rfl, or.inl (lt_one_iff_zero.1 ha)], },
+  { rintro (rfl | rfl),
+    exacts [le_of_lt zero_lt_one, le_refl _], }
+end
+
 /-! ### The predecessor of an ordinal -/
 
 /-- The ordinal predecessor of `o` is `o'` if `o = succ o'`,