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