Proof step 1 from proof mult-ls (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  n ≠ 0, m / n < n0, ¬ m < n0 * n ⊦

Rule argument

Additional information

Proof step 2 from proof mult-ls (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  n ≠ 0, m / n < n0, n0 * n ≤ m ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 3 from proof mult-ls (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 4:

  ⊦ n ≠ 0 → m / n * n ≤ m ∧ m < (m / n)+1 * n

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) ⊦ m * (n + 1) = m * n + m; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n → n ≠ 0; (s) ⊦ ¬ n < n; (s) ⊦ m * n < m1 * n + n ↔ m < m1 + 1 ∧ n ≠ 0; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult Used terms: n, m

Proof step 4 from proof mult-ls (previous step) (back to tree)

Lemma Divdef