proposition: Lemma Qpos_hprop (a b: Qpos) : proj1_sig a = proj1_sig b -> a = b.
proof: Proof. destruct a, b. intros H. simpl in H. subst x0. f_equal. exact (Zlt_hprop _ _ q q0). 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