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