There is discussion of something like this in the Euclid's Theorem tutorial. You can do Induct_on `j - i` or do the trick where you prove ?k. j = i + SUC k, eliminate j, and then induct on k.
Konrad. On Sat, Jan 5, 2019 at 12:35 PM Chun Tian (binghe) <binghe.l...@gmail.com> wrote: > sorry, "i ≤ j” should be “i < j” actually: > > ∀i j. i < j ⇒ f (SUC i) ⊆ f j > ------------------------------------ > 0. ∀n. f n ⊆ f (SUC n) > 1. ∀n. 0 < n ⇒ f 0 ⊆ f n > > > Il giorno 05 gen 2019, alle ore 19:32, Chun Tian (binghe) < > binghe.l...@gmail.com> ha scritto: > > > > Hi, > > > > I have the following goal to prove: (f : num -> ‘a set) > > > > ∀i j. i ≤ j ⇒ f (SUC i) ⊆ f j > > ------------------------------------ > > 0. ∀n. f n ⊆ f (SUC n) > > > > but how can I do the induction on … e.g. `j - i`? > > > > —Chun > > > > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info >
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
