- apply (ous_convex ?? H3 ? H11 (H6 (m 0)));
- simplify; repeat split; [intro X; cases (os_coreflexive ?? X)|2,3:apply H6;]
- change with (a (m O) ≤ a i);
- apply (trans_increasing ?? H4); intro; whd in H12;
- apply (not_le_Sn_n i); apply (transitive_le ??? H12 H5)]
+ cases H1;
+ [cases H5; cases H7; apply (ous_convex ?? H3 ? H11 (H12 (m O)));
+ |cases H5; cases H7; cases (us_phi4 ?? H3 〈(a (m O)),l〉);
+ lapply (H14 H11) as H11'; apply (ous_convex ?? H3 〈l,(a (m O))〉 H11' (H12 (m O)));]
+ 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);]]