@[reducible, inline]

abbrev Lean.Grind.isLt (x y : Nat) : Bool

Equations

• Lean.Grind.isLt x y = decide (x < y)

@[reducible, inline]

abbrev Lean.Grind.isLE (x y : Nat) : Bool

Equations

• Lean.Grind.isLE x y = decide (x ≤ y)

Theorems for transitivity.

theorem Lean.Grind.Nat.le_ro (u w v k : Nat) : u ≤ w → w ≤ v + k → u ≤ v + k

theorem Lean.Grind.Nat.le_lo (u w v k : Nat) : u ≤ w → w + k ≤ v → u + k ≤ v

theorem Lean.Grind.Nat.lo_le (u w v k : Nat) : u + k ≤ w → w ≤ v → u + k ≤ v

theorem Lean.Grind.Nat.lo_lo (u w v k₁ k₂ : Nat) : u + k₁ ≤ w → w + k₂ ≤ v → u + (k₁ + k₂) ≤ v

theorem Lean.Grind.Nat.lo_ro_1 (u w v k₁ k₂ : Nat) : isLt k₂ k₁ = true → u + k₁ ≤ w → w ≤ v + k₂ → u + (k₁ - k₂) ≤ v

theorem Lean.Grind.Nat.lo_ro_2 (u w v k₁ k₂ : Nat) : u + k₁ ≤ w → w ≤ v + k₂ → u ≤ v + (k₂ - k₁)

theorem Lean.Grind.Nat.ro_le (u w v k : Nat) : u ≤ w + k → w ≤ v → u ≤ v + k

theorem Lean.Grind.Nat.ro_lo_1 (u w v k₁ k₂ : Nat) : u ≤ w + k₁ → w + k₂ ≤ v → u ≤ v + (k₁ - k₂)

theorem Lean.Grind.Nat.ro_lo_2 (u w v k₁ k₂ : Nat) : isLt k₁ k₂ = true → u ≤ w + k₁ → w + k₂ ≤ v → u + (k₂ - k₁) ≤ v

theorem Lean.Grind.Nat.ro_ro (u w v k₁ k₂ : Nat) : u ≤ w + k₁ → w ≤ v + k₂ → u ≤ v + (k₁ + k₂)

Theorems for negating constraints.

theorem Lean.Grind.Nat.of_le_eq_false (u v : Nat) : (u ≤ v) = False → v + 1 ≤ u

theorem Lean.Grind.Nat.of_lo_eq_false_1 (u v : Nat) : (u + 1 ≤ v) = False → v ≤ u

theorem Lean.Grind.Nat.of_lo_eq_false (u v k : Nat) : (u + k ≤ v) = False → v ≤ u + (k - 1)

theorem Lean.Grind.Nat.of_ro_eq_false (u v k : Nat) : (u ≤ v + k) = False → v + (k + 1) ≤ u

Theorems for closing a goal.

theorem Lean.Grind.Nat.unsat_le_lo (u v k : Nat) : isLt 0 k = true → u ≤ v → v + k ≤ u → False

theorem Lean.Grind.Nat.unsat_lo_lo (u v k₁ k₂ : Nat) : isLt 0 (k₁ + k₂) = true → u + k₁ ≤ v → v + k₂ ≤ u → False

theorem Lean.Grind.Nat.unsat_lo_ro (u v k₁ k₂ : Nat) : isLt k₂ k₁ = true → u + k₁ ≤ v → v ≤ u + k₂ → False

Theorems for propagating constraints to True

theorem Lean.Grind.Nat.lo_eq_true_of_lo (u v k₁ k₂ : Nat) : isLE k₂ k₁ = true → u + k₁ ≤ v → (u + k₂ ≤ v) = True

theorem Lean.Grind.Nat.le_eq_true_of_lo (u v k : Nat) : u + k ≤ v → (u ≤ v) = True

theorem Lean.Grind.Nat.le_eq_true_of_le (u v : Nat) : u ≤ v → (u ≤ v) = True

theorem Lean.Grind.Nat.ro_eq_true_of_lo (u v k₁ k₂ : Nat) : u + k₁ ≤ v → (u ≤ v + k₂) = True

theorem Lean.Grind.Nat.ro_eq_true_of_le (u v k : Nat) : u ≤ v → (u ≤ v + k) = True

theorem Lean.Grind.Nat.ro_eq_true_of_ro (u v k₁ k₂ : Nat) : isLE k₁ k₂ = true → u ≤ v + k₁ → (u ≤ v + k₂) = True

Theorems for propagating constraints to False. They are variants of the theorems for closing a goal.

theorem Lean.Grind.Nat.lo_eq_false_of_le (u v k : Nat) : isLt 0 k = true → u ≤ v → (v + k ≤ u) = False

theorem Lean.Grind.Nat.le_eq_false_of_lo (u v k : Nat) : isLt 0 k = true → u + k ≤ v → (v ≤ u) = False

theorem Lean.Grind.Nat.lo_eq_false_of_lo (u v k₁ k₂ : Nat) : isLt 0 (k₁ + k₂) = true → u + k₁ ≤ v → (v + k₂ ≤ u) = False

theorem Lean.Grind.Nat.ro_eq_false_of_lo (u v k₁ k₂ : Nat) : isLt k₂ k₁ = true → u + k₁ ≤ v → (v ≤ u + k₂) = False

theorem Lean.Grind.Nat.lo_eq_false_of_ro (u v k₁ k₂ : Nat) : isLt k₁ k₂ = true → u ≤ v + k₁ → (v + k₂ ≤ u) = False

Helper theorems for equality propagation

theorem Lean.Grind.Nat.le_of_eq_1 (u v : Nat) : u = v → u ≤ v

theorem Lean.Grind.Nat.le_of_eq_2 (u v : Nat) : u = v → v ≤ u

theorem Lean.Grind.Nat.eq_of_le_of_le (u v : Nat) : u ≤ v → v ≤ u → u = v

theorem Lean.Grind.Nat.le_offset (a k : Nat) : k ≤ a + k