proposition: Lemma QabsQpos_correct x : ~x == 0 -> QabsQpos x == Qabs x.
proof: Proof. Proof with auto with qarith. intros E. destruct x as [n d]. simpl. destruct n... destruct E... Qed.
imports: Coq.QArith.QArith Coq.QArith.Qpower CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 Coq.Logic.Eqdep_dec CoRN.tactics.CornTac Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.Q