not 3 is square by PEPIN:41;
hence not for b₁ being Nat holds b₁ is square ; :: thesis: verum