Stream: math-comp users

Topic: Getting rid of ... \is Num.pos

view this post on Zulip Yves Bertot (May 19 2021 at 07:30):

When using ltf_pinv, I make goals of the form 'x \is Num.pos` appear, but I would need to have '0 < x' instead, so that I can go on writing on these goals. How do I do that?

view this post on Zulip Yves Bertot (May 19 2021 at 09:06):

I found the solution: lemma posrE

view this post on Zulip Laurent Théry (May 19 2021 at 12:37):

rewrite qualifE.

view this post on Zulip Yves Bertot (May 19 2021 at 12:42):

Ok thanks

Last updated: Oct 13 2024 at 01:02 UTC