proposition: Lemma Q_to_Z_to_Q_i : forall (z:Z), Q_to_Z_i (Z_to_Q_i z) = z.
proof: Proof. intros [|p|p]; trivial; simpl; rewrite Qpositive_to_positive_to_Qpositive_i; trivial. Defined.
imports: Coq(ZArith) Coq(Lia) QArithSternBrocot(Q_field)