Ugly computations with complex numbers

[SnarkBoojum]

Playing with complex numbers, I can't help but notice that some computations are pretty ugly:

From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp.real_closed Require Import complex realalg.

Import GRing GRing.Field.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Open Scope ring_scope.
Open Scope complex_scope.

Definition RR := { realclosure rat }.
Definition CC := complex RR.

Section EasyTests.

(* too ugly, report! *)
Compute Re (1+i*1).
Compute 'i * 'i.
Compute 'i + 'i.
Compute 'i^*.

End EasyTests.

There's also a lemma where I have the following line, just for 'i * 'i = -1:

rewrite -[(_ +i* _) * (_ +i* _)]/(_ +i* _) !mul0r mulr0 mulr1 !add0r complexr0 in H.

Perhaps there's something to be done to improve matters?

[CohenCyril]

Playing with complex numbers, I can't help but notice that some computations are pretty ugly:

Computations are not meant to work and cannot be made to work for such complex datatypes. The internal representation of algebraic numbers should not be exposed.

There's also a lemma where I have the following line, just for 'i * 'i = -1:

rewrite -[(_ +i* _) * (_ +i* _)]/(_ +i* _) !mul0r mulr0 mulr1 !add0r complexr0 in H.

There is a generic theorm: https://github.com/math-comp/math-comp/blob/1f0daa44f834a040367f5fcb44451571fc9b646b/mathcomp/algebra/ssrnum.v#L4382-L4383 Actually, many theorems for complex algebraic numbers are derived from the theory of numClosedField in mathcomp.algebra.ssrnum.