English
In PartENat, if c ≠ ⊤, then a + c = b + c iff a = b.
Русский
В PartENat, если c ≠ ⊤, то a + c = b + c тогда и только тогда, когда a = b.
LaTeX
$$$\\forall {a\\, b\\, c : \\mathrm{PartENat}},\\; c \\neq \\top \\Rightarrow (a + c = b + c \\iff a = b)$$$
Lean4
protected theorem add_right_cancel_iff {a b c : PartENat} (hc : c ≠ ⊤) : a + c = b + c ↔ a = b :=
by
rcases ne_top_iff.1 hc with ⟨c, rfl⟩
refine PartENat.casesOn a ?_ ?_ <;> refine PartENat.casesOn b ?_ ?_ <;>
simp [add_eq_top_iff, natCast_ne_top, @eq_comm _ (⊤ : PartENat), top_add]
simp only [← Nat.cast_add, add_left_cancel_iff, PartENat.natCast_inj, add_comm, forall_const]