proposition: Lemma Z_to_Qminus : forall x y : Z, Z_to_Q (x - y) = Qminus (Z_to_Q x) (Z_to_Q y).
proof: Proof. intros x y. unfold Zminus in |- *. rewrite Z_to_Qplus. rewrite Z_to_Qopp. reflexivity. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)