- 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);]]
+ 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);]]