Square obstructions in semireal rings

Semireality excludes -1 from the squares. The Fact instance supplies this obstruction when constructing a field by adjoining a square root of -1.

instance TauCeti.instFactNotIsSquareNegOfNat_tauCeti {R : Type u_1} [AddGroup R] [One R] [Mul R] [IsSemireal R] : Fact ¬IsSquare (-1)

In a semireal additive group with multiplication and a distinguished 1, -1 is not a square. This supplies the square obstruction used by quadratic-algebra field instances.