proposition: Lemma a_field_equality_4 : forall a b c d e f g h q1 q2 : Q, g <> Zero -> Qmult a g = Qmult c e -> Qmult b g = Qmult c f -> Qmult c h = Qmult d g -> Qplus (Qplus (Qplus (Qmult (Qmult e q1) q2) (Qmult f q1)) (Qmult g q2)) h <> Zero -> Qmult c (Qinv g) = Qmult (Qplus (Qplus (Qplus (Qmult (Qmult a q1) q2) (Qmult b q1)) (Qmult c q2)) d) (Qinv (Qplus (Qplus (Qplus (Qmult (Qmult e q1) q2) (Qmult f q1)) (Qmult g q2)) h)).
proof: Proof. intros a b c d e f g h p1 p2 He H4 H3 H2 Hdenom. symmetry in |- *. rewrite Qdiv_num_denom with (p := g); [ idtac | assumption ]. rewrite Q_distr_left. rewrite <- H2. rewrite Q_distr_left with (z := g). rewrite Q_distr_left with (z := g). replace (Qmult (Qmult b p1) g) with (Qmult (Qmult f p1) c). replace (Qmult (Qmult c p2) g) with (Qmult (Qmult g p2) c). replace (Qmult (Qmult (Qmult a p1) p2) g) with (Qmult (Qmult (Qmult e p1) p2) c). rewrite (Qmult_sym c h). rewrite <- Q_distr_left with (z := c). rewrite <- Q_distr_left with (z := c). rewrite <- Q_distr_left. rewrite Qmult_sym with (m := c). rewrite Qmult_sym with (m := g). rewrite <- Qdiv_num_denom; [ reflexivity | assumption ]. transitivity (Qmult (Qmult (Qmult c e) p1) p2); [ ring | rewrite <- H4; ring ]. ring. replace (Qmult (Qmult f p1) c) with (Qmult (Qmult c f) p1) by ring; rewrite <- H3; ring. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)