case refine_2.refine_2
a b : PartENat
⊢ ∀ (n n_1 : ℕ), ¬↑n_1 + ↑n = ⊤
a b : PartENat
⊢ a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤
refine PartENat.casesOn a ?_ ?_
<;> refine PartENat.casesOn b ?_ ?_
<;> simp
no goals
case refine_2.refine_2
a b : PartENat
⊢ ∀ (n n_1 : ℕ), ¬↑n_1 + ↑n = ⊤
simp only [←Nat.cast_add, PartENat.natCast_ne_top, forall_const]