proposition: Lemma Qabs_le_nonneg (x y : Q) : 0 <= x -> (Qabs x <= y <-> x <= y).
proof: Proof. intro A. rewrite Qabs_Qle_condition. split; [intros [_ ?]; trivial | intro A1; split; [| trivial]]. apply Qle_trans with (y := 0); [| trivial]. apply (Qopp_le_compat 0); eapply Qle_trans; eauto. 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