proposition: Lemma Z_to_Qpositive_Q_tail_pos : forall (a : Z) (Ha : (0 < a)%Z), Z_to_Qpositive a Ha = Q_tail a.
proof: Proof. intros [| px| px] Hx; discriminate Hx || reflexivity. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)