cases H1; [exists [apply O] apply H2;]
exists [apply (S O)] lapply (H O) as H3; rewrite < H2 in H3; assumption
|2: cases H1 (p Hp); cases (nat_discriminable (S n) (m p));
- [ cases H2; clear H2;
- [ exists [apply p]; assumption;
- | exists [apply (S p)]; rewrite > H3; apply H;]
- | cases (?:False); change in Hp with (n<m p);
-apply (not_le_Sn_n (m p) ?).
- apply (transitive_le (S (m p)) (S n) (m p) ? ?);
- [apply (H2).
- |apply (Hp).
- ]]]
+ [1: cases H2; clear H2;
+ [1: exists [apply p]; assumption;
+ |2: exists [apply (S p)]; rewrite > H3; apply H;]
+ |2: cases (?:False); change in Hp with (n<m p);
+ apply (not_le_Sn_n (m p));
+ apply (transitive_le ??? H2 Hp);]]
qed.
lemma selection:
cases (strictly_increasing_reaches C ? Hm w);
exists [apply w1]; cases (os_cotransitive ??? (a (m w1)) H); [2:assumption]
cases (trans_increasing C ? Ia ?? H1); assumption;]
-qed. (* dovevo usare il lemma 2.3! *)
+qed.