proposition: Lemma Rle_mult_nonpos_nonpos: forall r1 r2 : R, r1<=0 -> r2<=0 -> 0 <= r1 * r2.
proof: Proof. intros r1 r2 Hr1 Hr2; stepr ((-r1)*(-r2)); [|ring]; apply Rle_mult_nonneg_nonneg; lra. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)