proposition: Lemma Rabs_Rle: forall q p : R, (- p <= q)%R -> (q <= p)%R -> (Rabs q <= p)%R.
proof: Proof. intros q p H1 H2; assert (H_p: 0<= p); [lra|]; stepr (Rmax (Rabs (-p)) (Rabs p)); [ apply RmaxAbs; trivial | rewrite Rabs_Ropp; rewrite Rmax_involutive; apply Rabs_pos_eq; assumption]. Qed.
imports: Coq(Reals) Coq(Lra) Coq(Fourier) Coq(Euclid) Coq(Lia)