proposition: Lemma conjL_range_l:forall r, -1 <= r -> -1<= (r-1)/(r+3).
proof: Proof. intros r Hr; stepl (-1/1); [| field; apply R1_neq_R0]; apply Rmult_Rdiv_pos_Rle; try lra; rewrite Rmult_plus_distr_l; rewrite Rmult_1_r; lra. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)