Subject: Tactics

Keywords: ::tactic

Title: Rewriting with order relations.

--------------------------------------------------
With hypothesis 7. a ≤ b and conclusion a < c one can rewrite using RWO "7" 0
to get new conclusion b < c. But this will only work if the order family has
been declared (see rless family for an example). Also, as noted in the
comment there, functionality lemmas like rless_functionality_wrt_implies
must be made and the use of b ≥ a in that lemma seems to be essential.
That is, the whole family of relations must be defined (it does not work to
state the functionality lemma with a ≤ b in place of b ≥ a ). ⋅
--------------------------------------------------

Authors: MARK:t

⋅

Home