proposition: Lemma Rle_pos_nonneg_Rdiv: forall r1 r2 : R, 0 < r1 -> 0 <= r2 / r1 -> 0<= r2.
proof: Proof. intros r1 r2 Hr2 Hr12; unfold Rdiv in Hr12; apply Rle_pos_nonneg_Rmult with (/r1); auto. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)