-apply (le_rewl ??? (f+h+ -h) (plus_comm ? f h));
-apply (le_rewl ??? (f+(h+ -h)) (plus_assoc ????));
-apply (le_rewl ??? (f+(-h+h)) (plus_comm ? h (-h)));
-apply (le_rewl ??? (f+0) (opp_inverse ??));
-apply (le_rewl ??? (0+f) (plus_comm ???));
-apply (le_rewl ??? (f) (zero_neutral ??));
-apply (le_rewr ??? (g+h+ -h) (plus_comm ? h ?));
-apply (le_rewr ??? (g+(h+ -h)) (plus_assoc ????));
-apply (le_rewr ??? (g+(-h+h)) (plus_comm ??h));
-apply (le_rewr ??? (g+0) (opp_inverse ??));
-apply (le_rewr ??? (0+g) (plus_comm ???));
-apply (le_rewr ??? (g) (zero_neutral ??) H);
+apply (Le≪ (f+h+ -h) (plus_comm ? f h));
+apply (Le≪ (f+(h+ -h)) (plus_assoc ????));
+apply (Le≪ (f+(-h+h)) (plus_comm ? h (-h)));
+apply (Le≪ (f+0) (opp_inverse ??));
+apply (Le≪ (0+f) (plus_comm ???));
+apply (Le≪ (f) (zero_neutral ??));
+apply (Le≫ (g+h+ -h) (plus_comm ? h ?));
+apply (Le≫ (g+(h+ -h)) (plus_assoc ????));
+apply (Le≫ (g+(-h+h)) (plus_comm ??h));
+apply (Le≫ (g+0) (opp_inverse ??));
+apply (Le≫ (0+g) (plus_comm ???));
+apply (Le≫ (g) (zero_neutral ??) H);