proposition: Lemma Qpos_ind (P: T -> Prop) (Pwd: Proper (eq ==> iff) P) (P0: P 0) (Pp: forall q: Qpos, P (from_Qpos q)) : forall q, P q.
proof: Proof. Proof with auto. intro. apply rect; intros. apply (Pwd 0)... reflexivity. assert (0 < (Z.pos n # d)). reflexivity. apply (Pwd (from_Qpos (exist _ _ H0))). reflexivity. apply Pp. Qed.
imports: CoRN.model.totalorder.QposMinMax Coq.Program.Program CoRN.model.structures.QposInf Coq.QArith.Qminmax