∀ {x y z : ℤ} (hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0) (hp : (↑x / ↑z, ↑y / ↑z) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}),
  0 <
      ↑((circleEquivGen hQ).symm ⟨(↑x / ↑z, ↑y / ↑z), hp⟩).den ^ 2 +
        ((circleEquivGen hQ).symm ⟨(↑x / ↑z, ↑y / ↑z), hp⟩).num ^ 2 →
    2 ∣
          ↑((circleEquivGen hQ).symm ⟨(↑x / ↑z, ↑y / ↑z), hp⟩).den ^ 2 +
            ((circleEquivGen hQ).symm ⟨(↑x / ↑z, ↑y / ↑z), hp⟩).num ^ 2 ∧
        2 ∣
            ↑((circleEquivGen hQ).symm ⟨(↑x / ↑z, ↑y / ↑z), hp⟩).den ^ 2 -
              ((circleEquivGen hQ).symm ⟨(↑x / ↑z, ↑y / ↑z), hp⟩).num ^ 2 ∧
          (↑((circleEquivGen hQ).symm ⟨(↑x / ↑z, ↑y / ↑z), hp⟩).den ^ 2 -
                    ((circleEquivGen hQ).symm ⟨(↑x / ↑z, ↑y / ↑z), hp⟩).num ^ 2) /
                  2 %
                2 =
              0 ∧
            ((↑((circleEquivGen hQ).symm ⟨(↑x / ↑z, ↑y / ↑z), hp⟩).den ^ 2 -
                      ((circleEquivGen hQ).symm ⟨(↑x / ↑z, ↑y / ↑z), hp⟩).num ^ 2) /
                    2).gcd
                ((↑((circleEquivGen hQ).symm ⟨(↑x / ↑z, ↑y / ↑z), hp⟩).den ^ 2 +
                    ((circleEquivGen hQ).symm ⟨(↑x / ↑z, ↑y / ↑z), hp⟩).num ^ 2) /
                  2) =
              1 →
      0 <
        (↑((circleEquivGen hQ).symm ⟨(↑x / ↑z, ↑y / ↑z), hp⟩).den ^ 2 +
            ((circleEquivGen hQ).symm ⟨(↑x / ↑z, ↑y / ↑z), hp⟩).num ^ 2) /
          2