Near message error

[mkerjean]

While trying to solve e <= M for e : numFieldtype and M \is_near (nbhs +oo), one gets the error message no applicable tactic. A message including the necessity for e to be real (is this what's happening ?), or to try with normr e, would help a lot, would it be hard to implement?

[affeldt-aist]

While trying to solve e <= M for e : numFieldtype and M \is_near (nbhs +oo), one gets the error message no applicable tactic. A message including the necessity for e to be real (is this what's happening ?),

I guess so, since nbhs_pinfty_ge is registered as a Hint but requires e to verify \is Num.real for which e : R : numFieldType is not sufficient.

or to try with normr e, would help a lot, would it be hard to implement?

Do you mean by using as an intermediate step the lemma ler_norm? But the latter requires a realDomainType so numFieldType is anyway not enough. (I might be missing the point.)

[mkerjean]

While trying to solve e <= M for e : numFieldtype and M \is_near (nbhs +oo), one gets the error message no applicable tactic. A message including the necessity for e to be real (is this what's happening ?),

I guess so, since nbhs_pinfty_ge is registered as a Hint but requires e to verify \is Num.real for which e : R : numFieldType is not sufficient.

or to try with normr e, would help a lot, would it be hard to implement?

Do you mean by using as an intermediate step the lemma ler_norm? But the latter requires a realDomainType so numFieldType is anyway not enough. (I might be missing the point.)

I was suggesting that the error message might say "try using normr e instead of e" or something like that, but I wasn't sure how nbhs_pinfty_ge and similar lemmas were used. As this is with an Hint, can the error message be more precise ? How can we do that ?