fact: Definition QabsQpos (x : Q) : Qpos := match x with | 0 # _ => exist (Qlt 0) (1#1) eq_refl | (Zpos an) # ad => exist (Qlt 0) (Z.pos an # ad) eq_refl | (Zneg an) # ad => exist (Qlt 0) (Z.pos an # ad) eq_refl end.
imports: Coq.Logic.Eqdep_dec Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qpower Coq.QArith.Qround CoRN.model.totalorder.QMinMax CoRN.order.TotalOrder