Setup for the gcongr tactic

The core implementation of the gcongr ("generalized congruence") tactic is in the file Tactic.GCongr.Core. In this file we set it up for use across the library by tagging a minimal set of lemmas with the attribute @[gcongr] and by listing positivity as a first-pass discharger for side goals (gcongr_discharger).

≤, -

<, -

≤, +

<, +

≤, -

<, -

≤, *

<, *

≤, /

theorem Nat.div_le_div {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} (h1 : a ≤ b) (h2 : d ≤ c) (h3 : d ≠ 0) : a / c ≤ b / d

<, /

≤, ⁻¹

≤, ^

<, ^

theorem zpow_lt_of_lt {α : Type u_1} [LinearOrderedSemifield α] {a : α} {m : ℤ} {n : ℤ} (hx : 1 < a) (h : m < n) : a ^ m < a ^ n

coercions

theorem Nat.cast_le_cast {α : Type u_1} [OrderedSemiring α] [CharZero α] {x : ℕ} {y : ℕ} (h : x ≤ y) : ↑x ≤ ↑y