Is there a nice tactic for dealing with goals involving INR? for instance what the nicest way to solve
forall a b, 0 <= INR a * INR b? Do I have to use the lemmase manually ie
apply Rmult_le_pos;apply pos_INR.?
Manual proof is what I would do. But theoretically, this falls in the fragment handled by
psatz R. I have no idea, however, if the tactic already knows about
INR or if you have to massage the goal beforehand using some other tactic.
hmm, that kind of preprocessing sounds like what Trakt is aiming for...
psatz R does not seem to know about
INR. But doing
generalize (pos_INR a) (pos_INR b) beforehand suffices.
Last updated: Oct 03 2023 at 02:34 UTC