Theorem “A7.1.1 no”: ¬ (∃ x : ℤ • ∀ y : ℤ • y + 2 < 3 · x )
Proof:
    ¬ (∃ x : ℤ • ∀ y : ℤ • y + 2 < 3 · x )
  ≡⟨“Generalised De Morgan”⟩
    (∀ x : ℤ • ¬ ∀ y : ℤ • y + 2 < 3 · x )
  ≡⟨“Generalised De Morgan”⟩
    (∀ x : ℤ • ∃ y : ℤ • ¬ (y + 2 < 3 · x))
  ≡⟨ Subproof:
      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))
        ≡⟨ Evaluation ⟩
          (¬ (false))
        ≡⟨ “Negation of `false`” ⟩
          true








    ⟩
      true