proposition: Lemma Qpositive_to_Z_nonneg : forall x : Qpositive, (0 <= Qpositive_to_Z x)%Z.
proof: Proof. intros x; induction x as [x Hrecx| x Hrecx| ]; [ replace (Qpositive_to_Z (nR x)) with (1 + Qpositive_to_Z x)%Z; trivial; abstract lia | simpl in |- *; apply Z.le_refl | simpl in |- *; intro H; discriminate ]. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)