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