rpred expose the iinternal of Num.real about math-comp HOT 5 OPEN

What about rpredN/= ?

from math-comp.

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?

from math-comp.

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.

from math-comp.

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.

from math-comp.

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

from math-comp.