proposition: Lemma Z_to_Qle : forall x y : Z, (x <= y)%Z -> Qle x y.
proof: Proof. intros x y H. case (Z_le_lt_eq_dec _ _ H); intro H1. apply Qlt_le_weak; apply Z_to_Qlt; assumption. rewrite H1; unfold Qle in |- *; apply Qlt_irreflexive. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)