proposition: Lemma eq_Z_to_Q : forall x y : Z, Z_to_Q x = Z_to_Q y -> x = y.
proof: Proof. intros x y H. generalize (f_equal Q_to_Z H). intro H0. rewrite (Q_to_Z_to_Q x) in H0. rewrite (Q_to_Z_to_Q y) in H0. assumption. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)