Reals: Make "Rsqr x" and an alias for "x^2"

Some developments of the Reals library use a wild mix between Rsqr x (aka x²) and x^2. the field tactic supports (afaikt) only x^2 while most of the lemmas connecting x^2 and sqrt use Rsqr. Trigonometric lemmas use a mix of both. As a result many proofs have to convert between the two forms from time to time. Also proof search is made substantially harder by this.

I would suggest to clean this up by making Rsqr an alias for x^2. The small performance advantage given by Rsqr should not be significant and less important that cleanliness and usability of the library.

@silene, @thery : can you please comment on this, especially also on the performance implications e.g. in CoqInterval (I always used x^2 there btw.)

Start by reviewing the Reals library definitions involving Rsqr, x^2, and sqrt, then inspect the field tactic and the trigonometric lemmas mentioned in the issue. Check the performance implications for CoqInterval before proposing the cleanup; done requires agreement on the representation and consistent library behavior.