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