- simplify; repeat split; [1,6:intro X; cases (os_coreflexive ?? X)|*: try apply H12;]
- [1:change with (a (m O) ≤ a i);
- apply (trans_increasing ?? H6); intro; apply (le_to_not_lt ?? H4 H14);
- |2:change with (a i ≤ a (m O));
- apply (trans_decreasing ?? H6); intro; apply (le_to_not_lt ?? H4 H16);]]
+ simplify; repeat split;
+ [1,6: apply (le_reflexive l);
+ |2,5: apply (H12 (\fst (m 0)));
+ |3,8: apply (H12 i);
+ |4:change with (a (m O) ≤ a i);
+ apply (trans_increasing a H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H14);
+ |7:change with (a i ≤ a (m O));
+ apply (trans_decreasing ? H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);]]