proposition: Lemma Qabs_zero (x : Q) : Qabs x == 0 <-> x == 0.
proof: Proof. split; intro H; [| now rewrite H]. destruct (Q_dec x 0) as [[x_neg | x_pos] | x_zero]; [| | trivial]. + rewrite Qabs_neg in H; [| apply Qlt_le_weak; trivial]. now rewrite <- (Qopp_involutive x), H. + rewrite Qabs_pos in H; [| apply Qlt_le_weak]; trivial. 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