proposition: Lemma conjL_range_r:forall r, -1<=r -> r <= 1 -> (r-1)/(r+3) <= 0.
proof: Proof. intros r Hr1 Hr2; apply Ropp_le_cancel; stepl 0; try ring; unfold Rdiv; rewrite Ropp_mult_distr; apply Rle_mult_inv_pos; lra. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)