proposition: Lemma Rabs_le : forall a b, -b <= a <= b -> Rabs a <= b.
proof: Proof. intros a b; unfold Rabs; case Rcase_abs. - intros _ [it _]; apply Ropp_le_cancel; rewrite Ropp_involutive; exact it. - intros _ [_ it]; exact it. Qed.
imports: Rdefinitions Raxioms RIneq R_Ifp