+lemma fle_plusl: ∀G:ogroup. ∀f,g,h:G. f≤g → h+f≤h+g.
+intros (G f g h);
+apply (plus_cancr_le ??? (-h));
+apply (le_rewl ??? (f+h+ -h)); [apply feq_plusr;apply plus_comm;]
+apply (le_rewl ??? (f+(h+ -h)) (plus_assoc ????));
+apply (le_rewl ??? (f+(-h+h))); [apply feq_plusl;apply plus_comm;]
+apply (le_rewl ??? (f+0)); [apply feq_plusl; apply eq_symmetric; apply opp_inverse]
+apply (le_rewl ??? (0+f) (plus_comm ???));
+apply (le_rewl ??? (f) (eq_symmetric ??? (zero_neutral ??)));
+apply (le_rewr ??? (g+h+ -h)); [apply feq_plusr;apply plus_comm;]
+apply (le_rewr ??? (g+(h+ -h)) (plus_assoc ????));
+apply (le_rewr ??? (g+(-h+h))); [apply feq_plusl;apply plus_comm;]
+apply (le_rewr ??? (g+0)); [apply feq_plusl; apply eq_symmetric; apply opp_inverse]
+apply (le_rewr ??? (0+g) (plus_comm ???));
+apply (le_rewr ??? (g) (eq_symmetric ??? (zero_neutral ??)));
+assumption;
+qed.