proposition: Lemma Qpositive_to_Z_Qpositive_le : forall x y : Qpositive, (Qpositive_to_Z x < Qpositive_to_Z y)%Z -> Qpositive_le x y.
proof: Proof. intros x y. unfold Qpositive_le in |- *. functional induction (Qpositive_le_bool x y) ;intros; trivial. apply IHb. unfold Qpositive_to_Z in H;fold Qpositive_to_Z in H. lia. unfold Qpositive_to_Z in H;fold Qpositive_to_Z in H; generalize (Qpositive_to_Z_nonneg y);intros; apply False_ind;lia. unfold Qpositive_to_Z in H;fold Qpositive_to_Z in H; generalize (Qpositive_to_Z_nonneg y);intros; apply False_ind;lia. apply IHb. unfold Qpositive_to_Z in H;fold Qpositive_to_Z in H. lia. unfold Qpositive_to_Z in H;fold Qpositive_to_Z in H;discriminate. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)