- 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; cases (us_phi4 ?? H3 〈l,a i〉);
+ apply H15; change with (U 〈a i,l〉);
+ [apply (ous_convex_l C ? H3 ? H11 (H12 (m O)));
+ |apply (ous_convex_r C ? H3 ? H11 (H12 (m O)));]
+ [1:apply (H12 i);
+ |3: apply (le_reflexive l);
+ |4: apply (H12 i);
+ |2:change with (a (m O) ≤ a i);
+ apply (trans_increasing a H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);
+ |5:apply (H12 i);
+ |7:apply (ge_reflexive (l : hos_carr (os_r C)));
+ |8:apply (H12 i);
+ |6:change with (a i ≤ a (m O));
+ apply (trans_decreasing ? H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);]]