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