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