- Subst1Gen; Rewrite H in H9; Simpl in H9; Clear H x2.
- Rewrite <- lt_plus_minus in H9; [ Idtac | XAuto ].
- Rewrite <- lt_plus_minus_r in H9; XEAuto.
+ Subst1Gen; Rewrite H in H10; Simpl in H10; Clear H x3.
+ Rewrite <- lt_plus_minus in H10; [ Idtac | XAuto ].
+ Rewrite <- lt_plus_minus_r in H10; XEAuto.