valMinAbs_neg_of_ne_half — Mathlib

English

If 2*a.val ≠ n, then (-a).valMinAbs = - a.valMinAbs.

Русский

Если 2·a.val ≠ n, то (-a).valMinAbs = - a.valMinAbs.

LaTeX

$$$(ha : 2 * a.val \\neq n) \\Rightarrow (-a).valMinAbs = - a.valMinAbs$$$

Lean4

theorem valMinAbs_neg_of_ne_half (ha : 2 * a.val ≠ n) : (-a).valMinAbs = -a.valMinAbs :=
  by
  rcases eq_zero_or_neZero n with h | h
  · subst h
    rfl
  refine (valMinAbs_spec _ _).2 ⟨?_, ?_, ?_⟩
  · rw [Int.cast_neg, coe_valMinAbs]
  · rw [neg_mul, neg_lt_neg_iff]
    exact a.valMinAbs_mem_Ioc.2.lt_of_ne (mt a.valMinAbs_mul_two_eq_iff.1 ha)
  · linarith only [a.valMinAbs_mem_Ioc.1]

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