proposition: Lemma spec_Qquadratic_Qpositive_to_Q_p_One_unfolded : forall (a b c d e f g h : Z) (p : Qpositive), Qmult (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos p)) (Qpos One)) (Qmult b (Qpos p))) (Qmult c (Qpos One))) d) (Qinv (Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos p)) (Qpos One)) (Qmult f (Qpos p))) (Qmult g (Qpos One))) h)) = Qmult (Qplus (Qmult (a + b)%Z (Qpos p)) (c + d)%Z) (Qinv (Qplus (Qmult (e + f)%Z (Qpos p)) (g + h)%Z)).
proof: Proof. Proof spec_Qquadratic_Qpositive_to_Q_p_One. Lemma spec_Qquadratic_Qpositive_to_Q_One_p : forall (a b c d e f g h : Z) (p : Qpositive), spec_Qquadratic_Qpositive_to_Q a b c d e f g h One p = spec_Qhomographic_Qpositive_to_Q (a + c) (b + d) (e + g) (f + h) p. Proof. intros a b c d e f g h p; unfold spec_Qhomographic_Qpositive_to_Q, spec_Qquadratic_Qpositive_to_Q in |- *; repeat rewrite Z_to_Qplus; apply f_equal2 with Q Q; [ ring | apply f_equal with Q; ring ]. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)