proposition: Lemma Qabs_Qle x y: (Qabs x <= y) <-> (-y <= x <= y).
proof: Proof. Proof with intuition. split. split. rewrite <- (Qopp_opp x). apply Qopp_le_compat. apply Qle_trans with (Qabs (-x)). apply Qle_Qabs. rewrite Qabs_opp... apply Qle_trans with (Qabs x)... apply Qle_Qabs. intros. apply Qabs_case... rewrite <- (Qopp_opp y). apply Qopp_le_compat... Qed.
imports: Coq.QArith.QArith Coq.ZArith.ZArith Coq.NArith.NArith Coq.QArith.Qpower Coq.QArith.Qround Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.List