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