proposition: Lemma Qpos_POS_1 : forall (m : Z) (qp : Qpositive), Z_to_Q m = Qpos qp -> (0 < m)%Z.
proof: Proof. intros m qp Hm; apply pos_Z_to_Q; rewrite Hm; apply Qlt_zero_pos. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)