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?
I found the solution: lemma posrE
rewrite qualifE.
Ok thanks
Last updated: Apr 17 2024 at 22:01 UTC