case inl
ho : 0 ≤ 1
⊢ Principal (fun x x_1 => x + x_1) 0

case inr
ho : 1 ≤ 1
⊢ Principal (fun x x_1 => x + x_1) 1
o : Ordinal
ho : o ≤ 1
⊢ Principal (fun x x_1 => x + x_1) o
rcases le_one_iff.1 ho with (rfl | rfl)
no goals
case inl
ho : 0 ≤ 1
⊢ Principal (fun x x_1 => x + x_1) 0
exact principal_zero
no goals
case inr
ho : 1 ≤ 1
⊢ Principal (fun x x_1 => x + x_1) 1
exact principal_add_one