proposition: Lemma conjR_range_weak:forall r, -1 <= r <= 1-> -1<= (r+1)/(-r+3)<=1.
proof: Proof. intros r [Hr1 Hr2]; split. apply Rle_trans with 0; try lra; apply conjR_range_l; trivial. apply conjR_range_r; trivial. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)