agda(arithmetic): Phase 1.3 ⊕-mono-<-right via right-recursive _⊕_

agda(arithmetic): Phase 1.3 ⊕-mono-<-right via right-recursive _⊕_ #27