rpred expose the iinternal of Num.real

[thery]

I am porting my code to mathcomp2.1

Here is the initial code :

From mathcomp Require Import all_ssreflect all_algebra all_field.
Open Scope ring_scope.

Import GRing.Theory.

Lemma  CrealN1  :  -1 \is Creal.
Proof. by  rewrite rpredN. Qed.

rpredN turns into -1 \is Creal into 1 \is Creal which is solved automatically.

With mathcomp2.1

Lemma CrealN1 : (-1 : algC) \is Num.real.
Proof.
rewrite rpredN.

Now repdN exposes the interval

1 \in Num.Internals.Def_Rreal_pred__canonical__GRing_OppClosed Algebraics.Implementation_type__canonical__Num_NumDomain

and the proof does not terminate anymore with by [].
What has changed?

[proux01]

What about rpredN/= ?

[thery]

It improves things but still by [] does not close the goal. We get

1 \in Num.Def.Rreal_pred

Anyway there is something weird. Now I write x \is Num.real and x \is a Num.nat. Should it not be x \is a Num.real?

[proux01]

It improves things but still by [] does not close the goal. We get

1 \in Num.Def.Rreal_pred

You may have to add something like rewrite qualifE/=

Anyway there is something weird. Now I write x \is Num.real and x \is a Num.nat. Should it not be x \is a Num.real?

I think both are accepted as input but it should indeed be the second when printing.

[thery]

qualifEreally opens the predicate I dont want this.
Here is my current proof.

From mathcomp Require Import all_ssreflect all_algebra all_field.

Open Scope ring_scope.

Goal (- 1 : algC) \is Num.real.
rewrite GRing.rpredN.
by rewrite -[_ \in _]/(_ \is Num.real).
Qed.

[proux01]

I see, I don't think we have a better solution currently.