4.1 13

Theorem “≤-Monotonicity of ·”:
   0 ≤ d  ⇒  a ≤ b  ⇒  a · d ≤ b · d
Proof:
    0 ≤ d  ⇒  a ≤ b  ⇒  a · d ≤ b · d
  ≡⟨ “Definition of ≤” ⟩
    0 < d ∨ 0 = d  ⇒  a ≤ b  ⇒  a · d ≤ b · d
  ≡⟨ Subproof:
      Assuming `0 < d ∨ 0 = d`, `a ≤ b`:
        By cases: `0 < d`, `0 = d`
           Completeness: By Assumption `0 < d ∨ 0 = d`
           Case `0 < d`:
               a · d ≤ b · d
             ≡⟨ “≤-Isotonicity of ·” with Assumption `0 < d`,
                Assumption `a ≤ b` ⟩
               true
           Case `d = 0`:
               a · d ≤ b · d
             ≡⟨ Assumption `0 = d` ⟩
               a · 0 ≤ b · 0
             ≡⟨ “Zero of ·”,
                “Reflexivity of ≤” ⟩
               true
    ⟩
      true