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