proposition: Lemma lt_Z_to_Q : forall x y : Z, Qlt (Z_to_Q x) (Z_to_Q y) -> (x < y)%Z.
proof: Proof. intros x y H. case (Z_dec' x y). intros [H1| H1]; trivial. apply False_ind. apply Qlt_irreflexive with x. apply Qlt_transitive with y; trivial. apply Z_to_Qlt; assumption. intro H1. apply False_ind. rewrite H1 in H. generalize H. apply Qlt_irreflexive. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)