Theorem “A7.1.1 no”: ¬ (∃ x : ℤ • ∀ y : ℤ • y + 2 < 3 · x )
Proof:
  Using “Generalised De Morgan”:
    Subproof for `(∀ x : ℤ • ∃ y : ℤ • ¬ (y + 2 < 3 · x) )`:
      For any `x : ℤ`:
          ∃ y : ℤ • ¬ (y + 2 < 3 · x)
        ⇐ ⟨“∃-Introduction”⟩
          (¬ (y + 2 < 3 · x))[y ≔ 3 · x]
        = ⟨ Substitution⟩
          (¬ (3 · x + 2 < 3 · x))
        = ⟨ “Identity of +”⟩
          (¬ (3 · x + 2 < 3 · x + 0))
        = ⟨ “<-Isotonicity of +”⟩
          (¬ (2 < 0))
        ≡ ⟨ Fact `2 < 0 ≡ false`⟩
          (¬ false)
        ≡ ⟨ “Negation of `false`”⟩
          true




Theorem “A7.1.2 yes”: (∀ x : ℤ • ∀ y : ℤ • ∃ z : ℤ • y + 2 · z ≤ z + 3 · x + 5)
Proof:
    (∀ x : ℤ • ∀ y : ℤ • ∃ z : ℤ • y + 2 · z ≤ z + 3 · x + 5)
  =⟨ Subproof for `(∀ x : ℤ • ∀ y : ℤ • ∃ z : ℤ • y + 2 · z ≤ z + 3 · x + 5)`:
          For any `x`:
              For any `y`:
                  ∃ z : ℤ • y + 2 · z ≤ z + 3 · x + 5
                ⇐⟨“∃-Introduction”⟩
                  (y + 2 · z ≤ z + 3 · x + 5)[z ≔ 3 · x + 5 - y]
                =⟨ Substitution⟩
                  (y + 2 · (3 · x + 5 - y) ≤ 3 · x + 5 - y + 3 · x + 5)
                =⟨ “Subtraction”⟩
                  (y + 2 · (3 · x + 5 + - y) ≤ 3 · x + 5 + - y + 3 · x + 5)
                =⟨ “Distributivity of · over +”⟩
                  (y + 2 · 3 · x + 2 · 5 + 2 · (- y) ≤ (3 + 3)· x + 5 + - y + 5)
                =⟨ Evaluation⟩
                  (y + 6· x + 10 + 2 · (- y) ≤ 6 · x + - y + 10)
                =⟨ Evaluation⟩
                  (y + 6· x + 10 + 2 · (- y) ≤ 6 · x +  - y + 10)
                =⟨ (15.21)⟩
                  (y + 6· x + 10 + (- 2) · y ≤ 6 · x  + - y + 10)
                =⟨ “Identity of ·”, “Distributivity of · over +”⟩
                  (6· x + 10 + (1 + (- 2)) · y ≤ 6 · x  + - y + 10)
                =⟨ “Subtraction”, Fact `1 - 2 = - 1`⟩
                  (6· x + 10 + (- 1) · y ≤ 6 · x - y + 10)
                =⟨ (15.20) ⟩
                  (6· x + 10 + (- y) ≤ 6 · x - y + 10)
                =⟨ “Symmetry of +” ⟩
                  (6· x  + (- y) + 10 ≤ 6 · x - y + 10)
                =⟨ “Subtraction” ⟩
                  (6· x - y + 10 ≤ 6 · x - y + 10)
                =⟨ “Reflexivity of ≤” ⟩
                   true
     ⟩
     true