proposition: Lemma Rlt_mult_pos_neg: forall r1 r2 : R, r1 < 0 -> 0<r2 -> r1 * r2<0.
proof: Proof. intros r1 r2 Hr1 Hr2; apply Ropp_lt_cancel; stepl R0; [|ring]; stepr ((-r1)*r2); [|ring]; apply Rlt_mult_pos_pos; auto. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)