proposition: Lemma positive_to_Qpositive_to_positive_i : forall qp, positive_to_Qpositive_i (Qpositive_to_positive_i qp) = qp.
proof: Proof. intros p; induction p as [p|p|]; trivial; simpl; rewrite IHp; trivial. Defined.
imports: Coq(ZArith) Coq(Lia) QArithSternBrocot(Q_field)