- |*: cut (u ≤ S n1 ∨ S n1 < u);
- [2,4: cases (cmp_nat u (S n1));
- [1,4: left; apply lt_to_le; assumption
- |2,5: rewrite > H7; left; apply le_n
- |3,6: right; assumption ]
- |*: cases Hcut; clear Hcut
- [1,3: left; split; [1,3: assumption |2: symmetry; assumption]
- cut (u = S n1); [2: apply le_to_le_to_eq; assumption ]
- clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut;
- cut (s = S (fst (a w)));
- [2: apply le_to_le_to_eq; [2: assumption]
- change in H8 with (s + n1 ≤ S (n1 + fst (a w)));
- rewrite > plus_n_Sm in H8; rewrite > sym_plus in H8;
- apply (le_plus_to_le ??? H8);]
- cases (H3 (a w) H6);
- change with (s = fst (a w1));
- change in H4 with (fst (a w) < fst (a w1));
- apply le_to_le_to_eq; [ rewrite > Hcut; assumption ]
- apply (os_le_to_nat_le (fst (a w1)) s (H2 w1));
- |*: right; split; try assumption;
- [1: rewrite > sym_plus in ⊢ (? ? %);
- rewrite < H6; apply le_plus_r; assumption;
- |2: cases (H3 (a w) H6);
- change with (s + S n1 ≤ u + fst (a w1));rewrite < plus_n_Sm;
- apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm;
- apply (le_plus ???? (le_n ?) H9);]]]]]
+ |*: cases (cmp_nat u (S n1));
+ [1,3: left; split; [1,3: assumption |2: assumption]
+ cut (u = S n1); [2: apply le_to_le_to_eq; assumption ]
+ clear H7 H5 H4;rewrite > Hcut in H8:(? ? (? % ?)); clear Hcut;
+ cut (s = S (\fst (a w)));
+ [2: apply le_to_le_to_eq; [2: assumption]
+ change in H8 with (s + n1 ≤ S (n1 + \fst (a w)));
+ rewrite > plus_n_Sm in H8; rewrite > sym_plus in H8;
+ apply (le_plus_to_le ??? H8);]
+ cases (H3 (a w) H6);
+ change with (s = \fst (a w1));
+ change in H4 with (\fst (a w) < \fst (a w1));
+ apply le_to_le_to_eq; [ rewrite > Hcut; assumption ]
+ apply (os_le_to_nat_le (\fst (a w1)) s (H2 w1));
+ |*: right; split; try assumption;
+ [1: rewrite > sym_plus in ⊢ (? ? %);
+ rewrite < H6; apply le_plus_r; assumption;
+ |2: cases (H3 (a w) H6);
+ change with (s + S n1 ≤ u + \fst (a w1));rewrite < plus_n_Sm;
+ apply (trans_le ??? (le_S_S ?? H8)); rewrite > plus_n_Sm;
+ apply (le_plus ???? (le_n ?) H9);]]]]