tsub — Mathlib

English

If m and n are even, then m − n is even.

Русский

Если m и n чётные, то m − n чётное.

LaTeX

$$$\text{Even}(m) \land \text{Even}(n) \Rightarrow \text{Even}(m - n)$$$

Lean4

theorem tsub [AddLeftReflectLE α] {m n : α} (hm : Even m) (hn : Even n) : Even (m - n) :=
  by
  obtain ⟨a, rfl⟩ := hm
  obtain ⟨b, rfl⟩ := hn
  refine ⟨a - b, ?_⟩
  obtain h | h := le_total a b
  · rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero]
  · exact (tsub_add_tsub_comm h h).symm

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