- |elim H;elim (decidable_eq_nat a t)
- [apply (ex_intro ? ? (S a));intros;intro;elim (in_cons_case ? ? ? ? H4)
- [rewrite < H5 in H2;rewrite < H2 in H3;apply (not_le_Sn_n ? H3)
- |elim H5;elim (H1 m ? H7);apply (le_S_S_to_le ? ? (le_S ? ? H3))]
- |cut ((leb a t) = true \lor (leb a t) = false)
- [elim Hcut
- [apply (ex_intro ? ? (S t));intros;intro;
- elim (in_cons_case ? ? ? ? H5)
- [rewrite > H6 in H4;apply (not_le_Sn_n ? H4)
- |elim H6;elim (H1 m ? H8);apply (trans_le a t m)
- [lapply (leb_to_Prop a t);rewrite > H3 in Hletin;assumption
- |apply (le_S_S_to_le t m (le_S (S t) m H4))]]
- |apply (ex_intro ? ? a);intros;intro;elim (in_cons_case ? ? ? ? H5)
- [lapply (leb_to_Prop a t);rewrite > H3 in Hletin;
- simplify in Hletin;lapply (not_le_to_lt ? ? Hletin);
- unfold in Hletin1;rewrite < H6 in Hletin;apply (Hletin H4)
- |elim H6;elim (H1 ? H4 H8)]]
- |elim (leb a t);autobatch]]]]
+ |elim H;
+ apply (ex_intro ? ? (S (max a t))).
+ intros.unfold. intro.
+ elim (in_cons_case ? ? ? ? H3)
+ [rewrite > H4 in H2.autobatch
+ |elim H4.apply (H1 m ? H6).
+ apply (trans_le ? (max a t));autobatch]]]