Description: In a right ordered monoid, the ordering is compatible with group addition. (Contributed by Thierry Arnoux, 30-Jan-2018)