- [ apply (nat_case1 n)
- [ intros.
- rewrite > H2 in H:(? ? %).
- change in H:(? ? %) with (O).
- change in H:(%) with ((S i) \le O).
- apply False_ind.
- apply (not_le_Sn_O i H)
- | intro.
- elim m
- [ rewrite > H2 in H1:(%).
- rewrite > H2 in H:(%).
- simplify in H.
- cut (i = O)
- [ rewrite > Hcut in H1:(%).
- simplify in H1.
- apply False_ind.
- apply (not_eq_true_false H1)
- | change in H:(%) with((S i) \le (S O)).
- cut (i \le O )
- [ apply (nat_case1 i)
- [ intros.
- reflexivity
- | intros.
- rewrite > H3 in Hcut:(%).
- apply False_ind.
- apply (not_le_Sn_O m1 Hcut)
- ]
- | apply (le_S_S_to_le i O).
- assumption
- ]
- ]
- | change with ((S O) \le (S n1)).
- apply (le_S_S O n1).
- apply (le_O_n n1)
- ]
- ]