proposition: Lemma a_field_equality_1 : forall x y z t w : Q, Qmult x t = Qmult y z -> t <> Zero -> Qplus (Qmult z w) t <> Zero -> Qmult (Qplus (Qmult x w) y) (Qinv (Qplus (Qmult z w) t)) = Qmult y (Qinv t).
proof: Proof. intros a b c d p H_xt_eq_yz Ht H_denom; rewrite Qdiv_num_denom with (p := d); [ idtac | assumption ]; replace (Qmult (Qplus (Qmult a p) b) d) with (Qplus (Qmult (Qmult a d) p) (Qmult b d)); [ idtac | ring ]; rewrite H_xt_eq_yz; field; auto. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)