proposition: Lemma Qabs_nonpos (x : Q) : Qabs x <= 0 -> x == 0.
proof: Proof. intro H. apply Qle_lteq in H. destruct H as [H | H]. + elim (Qlt_not_le _ _ H (Qabs_nonneg x)). + now apply Qabs_zero. 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