proposition: Lemma Q_Qpos_max : forall (x y:Qpos), proj1_sig (Qpos_max x y) == Qmax (proj1_sig x) (proj1_sig y).
proof: Proof. intros x y. unfold Qpos_max. unfold Qmax. unfold Default.max. destruct (Qpos_le_total y x) as [H|H]; destruct (Qle_total (proj1_sig y) (proj1_sig x)) as [H0|H0]; try reflexivity; apply Qle_antisym; auto. 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