proposition: Lemma add_monotony x y z : y <= z -> x + y <= x + z.
proof: Proof. by move=> leyz b [a ltxa /leyz]; exists a. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)