proposition: Lemma rect (P: T -> Type) (P0: forall (d: positive) H, P (exist (Qle 0) (0#d) H)) (Pp: forall (n d: positive) H, P (exist (Qle 0) (Zpos n#d) H)): forall q, P q.
proof: Proof. intros [[qn qd] E]. destruct qn. apply P0. apply Pp. exfalso. apply E. reflexivity. Defined.
imports: CoRN.model.totalorder.QposMinMax Coq.Program.Program CoRN.model.structures.QposInf Coq.QArith.Qminmax