even_sub — Mathlib

English

If n ≤ m, then m − n is even iff m and n have the same parity.

Русский

Если n ≤ m, то m − n чётно тогда и только тогда, когда m и n имеют одинаковую чётность.

LaTeX

$$$\forall m,n \in \mathbb{N},\ n \le m \Rightarrow \operatorname{Even}(m-n) \iff (\operatorname{Even}(m) \iff \operatorname{Even}(n))$$$

Lean4

@[parity_simps]
theorem even_sub (h : n ≤ m) : Even (m - n) ↔ (Even m ↔ Even n) := by grind

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