... also meant to mention that "Induct_on" and "completeInduct_on" have online documentation.
On Sat, Jan 5, 2019 at 3:20 PM Konrad Slind <konrad.sl...@gmail.com> wrote: > 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
