proposition: Lemma Q_to_Z_monotone : forall x y : Q, Qlt x y -> (Q_to_Z x <= Q_to_Z y)%Z.
proof: Proof. intros x y. unfold Qlt in |- *. intro H. induction H; simpl in |- *; apply not_Zlt; intro H1. apply H; apply Qpositive_to_Z_Qpositive_le; assumption. generalize (Zmin_cancel_Zlt _ _ H1); intro H2; apply H; apply Qpositive_to_Z_Qpositive_le; assumption. apply Z.lt_irrefl with 0%Z; generalize (Qpositive_to_Z_nonneg x'); intro H2; lia. apply Z.lt_irrefl with 0%Z; generalize (Qpositive_to_Z_nonneg x'); generalize (Qpositive_to_Z_nonneg y'); intros H2 H3; abstract lia. apply Z.lt_irrefl with 0%Z; generalize (Qpositive_to_Z_nonneg x'); intro H2; lia. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)