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