proposition: Lemma Qle_Qpositive_le_pos : forall x y : Qpositive, Qle (Qpos x) (Qpos y) -> Qpositive_le x y.
proof: Proof. intros x y H. case (Qpositive_le_dec x y); intros H1; trivial; apply False_ind; apply H; constructor; assumption. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)