proposition: Lemma spec_Qquadratic_Qpositive_to_Q_p_One : 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 p One = spec_Qhomographic_Qpositive_to_Q (a + b) (c + d) (e + f) (g + h) p.
proof: 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)