proposition: Lemma Qpos_nonzero : forall a:Qpos, ~(proj1_sig a == 0).
proof: Proof. intros. intro abs. destruct a. simpl in abs. rewrite abs in q. exact (Qlt_irrefl 0 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