proposition: Lemma conjRinv_range_r:forall r, 0<=r-> r <= 1 -> (3*r-1)/(r+1)<=1.
proof: Proof. intros r Hr1 Hr2. stepr (1/1); [| field; apply R1_neq_R0]; apply Rmult_Rdiv_pos_Rle; try lra; rewrite Rmult_1_r; rewrite Rmult_1_l; lra. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)