proposition: Lemma mul_monotony x y z : 0 <= x -> y <= z -> x * y <= x * z.
proof: Proof. move=> le0x leyz; set xy := mul x y; pose t := add (- y) z. have le0t: 0 <= t by rewrite -(addN y) addC; apply: add_monotony. rewrite -(add0 z) -(addN y) -addA -/t mulDr -[xy]add0 addC -/xy. by rewrite ge0_mul => [|/le0x|/le0t] //; apply/add_monotony/leRq/amul_ge0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)