take SQ R ; :: thesis: SQ R is with_squares
thus SQ R is with_squares ; :: thesis: verum