proposition: Lemma Qpos_eq_le_def : forall (x y: Qpos), proj1_sig x == proj1_sig y <-> proj1_sig x <= proj1_sig y /\ proj1_sig y <= proj1_sig x.
proof: Proof. intros. split. intros H; rewrite -> H. firstorder using Qle_refl. firstorder using Qle_antisym. 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