- apply (Eq≈ (0 + δ(an n3) (xn n3)) ? (zero_neutral ??));
- apply (Eq≈ (δ(an n3) (xn n3) + 0) ? (plus_comm ???));
- apply (Eq≈ (δ(an n3) (xn n3) + (-δ(xn n3) (bn n3) + δ(xn n3) (bn n3))) ? (opp_inverse ??));
- apply (Eq≈ (δ(an n3) (xn n3) + (δ(xn n3) (bn n3) + -δ(xn n3) (bn n3))) ? (plus_comm ?? (δ(xn n3) (bn n3))));
- apply (Eq≈ ? ? (eq_sym ??? (plus_assoc ????))); assumption;] clear H10;
- apply (le_rewl ??? ( δ(an n3) (xn n3)+ δ(an n3) x) (msymmetric ??(an n3)(xn n3)));
- apply (le_rewl ??? (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x) H11);
+ lapply (le_mtri ????? H7 H8) as H9; clear H7 H8;
+ lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? H9) as H10; clear H9;
+ apply (Eq≈ (0 + δ(an n3) (xn n3)) ? (zero_neutral ??));
+ apply (Eq≈ (δ(an n3) (xn n3) + 0) ? (plus_comm ???));
+ apply (Eq≈ (δ(an n3) (xn n3) + (-δ(xn n3) (bn n3) + δ(xn n3) (bn n3))) ? (opp_inverse ??));
+ apply (Eq≈ (δ(an n3) (xn n3) + (δ(xn n3) (bn n3) + -δ(xn n3) (bn n3))) ? (plus_comm ?? (δ(xn n3) (bn n3))));
+ apply (Eq≈ ?? (eq_sym ??? (plus_assoc ????))); assumption;]
+ apply (Le≪ (δ(an n3) (xn n3)+ δ(an n3) x) (msymmetric ??(an n3)(xn n3)));
+ apply (Le≪ (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x) H11);