proposition: Lemma Qpos_positive_numerator_rect (P: Qpos -> Type): (forall (a b: positive), P (a # b)%Qpos) -> forall q, P q.
proof: Proof. intros H q. destruct (Qpos_as_positive_ratio q). subst. apply H. Defined.
imports: Coq.QArith.QArith Coq.QArith.Qpower CoRN.model.ordfields.Qordfield CoRN.algebra.COrdFields2 Coq.Logic.Eqdep_dec CoRN.tactics.CornTac Coq.QArith.Qround Coq.QArith.Qabs CoRN.stdlib_omissions.Q