proposition: Lemma Rle_zero_Rminus : forall r1 r2:R , 0 <= r1-r2 -> r2 <= r1.
proof: Proof. intros r1 r2 H; apply RIneq.Rminus_le; apply RIneq.Ropp_le_cancel;rewrite RIneq.Ropp_minus_distr; rewrite RIneq.Ropp_0; assumption. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)