proposition: Lemma spec_Qquadratic_Qpositive_to_Q_One_p_unfolded : forall (a b c d e f g h : Z) (p : Qpositive), Qmult (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos One)) (Qpos p)) (Qmult b (Qpos One))) (Qmult c (Qpos p))) d) (Qinv (Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos One)) (Qpos p)) (Qmult f (Qpos One))) (Qmult g (Qpos p))) h)) = Qmult (Qplus (Qmult (a + c)%Z (Qpos p)) (b + d)%Z) (Qinv (Qplus (Qmult (e + g)%Z (Qpos p)) (f + h)%Z)).
proof: Proof. Proof spec_Qquadratic_Qpositive_to_Q_One_p. Lemma spec_Qquadratic_Qpositive_to_Q_nR_nR : forall (a b c d e f g h : Z) (p1 p2 : Qpositive), spec_Qquadratic_Qpositive_to_Q a b c d e f g h (nR p1) (nR p2) = spec_Qquadratic_Qpositive_to_Q a (a + b) (a + c) (a + b + c + d) e (e + f) (e + g) (e + f + g + h) p1 p2. Proof. intros. unfold spec_Qquadratic_Qpositive_to_Q in |- *. do 6 rewrite Qmult_Z_nR. rewrite Qpos_nR. repeat rewrite <- Qplus_assoc. repeat rewrite Z_to_Qplus. apply f_equal2 with Q Q. abstract ring. apply f_equal with Q. abstract ring. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)