proposition: Lemma Rplus_min_distr_r : forall a b c, Rmin b c + a = Rmin (b + a) (c + a).
proof: Proof. intros a b c. rewrite <- 3!(Rplus_comm a). apply Rplus_min_distr_l. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)