cases (H1 ? Gw) (ma Hma); cases (H2 ? Gw) (mb Hmb); clear H1 H2;
exists [apply (ma + mb)] intros; apply (HV 〈l,(x i)〉);
unfold; simplify; exists [apply (a i)] split;
-[2: apply (ous_convex ?? Gv 〈a i,b i〉); cases (H i) (Lax Lxb); clear H;
+[2: apply (ous_convex_l ?? Gv 〈a i,b i〉); cases (H i) (Lax Lxb); clear H;
[1: apply HW; exists [apply l]simplify; split;
[1: cases (us_phi4 ?? Gw 〈(a i),l〉); apply H2; clear H2 H;
apply (Hma i); rewrite > sym_plus in H1; apply (le_w_plus mb); assumption;
|2: apply Hmb; apply (le_w_plus ma); assumption]
- |2: simplify; apply (le_transitive ???? Lax Lxb);
- |3: simplify; repeat split; try assumption;
- [1: apply (le_transitive ???? Lax Lxb);
- |2: intro X; cases (os_coreflexive ?? X)]]
+ |2,3: simplify; apply (le_transitive (a i) ?? Lax Lxb);
+ |4: apply (le_reflexive);
+ |5,6: assumption;]
|1: apply HW; exists[apply l] simplify; split;
[1: apply (us_phi1 ?? Gw); unfold; apply eq_reflexive;
|2: apply Hma; rewrite > sym_plus in H1; apply (le_w_plus mb); assumption;]]