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