proposition: Lemma Rmax_mult : forall a b c, 0 <= c -> Rmax a b * c = Rmax (a * c) (b * c).
proof: Proof. intros. repeat rewrite (Rmult_comm _ c). apply sym_eq. apply RmaxRmult. apply H. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)