case inl
o : Ordinal
ho : o ≠ 0
hb : 0 ≤ 1
⊢ CNF 0 o = [(0, o)]

case inr
o : Ordinal
ho : o ≠ 0
hb : 1 ≤ 1
⊢ CNF 1 o = [(0, o)]
b o : Ordinal
hb : b ≤ 1
ho : o ≠ 0
⊢ CNF b o = [(0, o)]
rcases le_one_iff.1 hb with (rfl | rfl)
no goals
case inl
o : Ordinal
ho : o ≠ 0
hb : 0 ≤ 1
⊢ CNF 0 o = [(0, o)]
exact zero_CNF ho
no goals
case inr
o : Ordinal
ho : o ≠ 0
hb : 1 ≤ 1
⊢ CNF 1 o = [(0, o)]
exact one_CNF ho