Proof step 1 from proof nummult-modle (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  j % i = 0, ¬(i * i0 ≤ j * j0 ↔ i0 ≤ j / i * j0), i < j, 0 < i ⊦

Rule argument

Additional information

Proof step 2 from proof nummult-modle (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  j % i = 0, ¬(i * i0 ≤ j * j0 ↔ i0 ≤ j / i * j0), 1 < j, i < j, 0 < i, 0 < j ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1

Proof step 3 from proof nummult-modle (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  ⊦ 0 < j ∧ 0 < i → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ 0 ≤ j0 ∧ j0 < j)

Rule argument

Additional information

Used simplifier rules: ⊦ i + 0 = i; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ 0 < i → (i * j ≤ i * i0 ↔ j ≤ i0); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j, i, i1, j1

Proof step 4 from proof nummult-modle (previous step) (back to tree)

Lemma div-elim