proposition: Lemma Qpos_red_eq : forall (a b : Qpos), QposEq a b -> Qpos_red a = Qpos_red b.
proof: Proof. intros p q H. apply Qpos_hprop. simpl. apply Qred_complete. exact H. 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