proposition: Lemma Qpos_ispos : forall a:Qpos, 0 < proj1_sig a.
proof: Proof. intros. destruct a; exact q. Qed.
imports: Coq.Logic.Eqdep_dec Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qpower Coq.QArith.Qround CoRN.model.totalorder.QMinMax CoRN.order.TotalOrder