add_right_cancel_iff — Mathlib

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]

Похожие утверждения