proposition: Lemma spec_Qquadratic_Qpositive_to_Q_dL_nR_unfolded : forall (a b c d e f g h : Z) (p1 p2 : Qpositive), Qmult (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos (dL p1))) (Qpos (nR p2))) (Qmult b (Qpos (dL p1)))) (Qmult c (Qpos (nR p2)))) d) (Qinv (Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos (dL p1))) (Qpos (nR p2))) (Qmult f (Qpos (dL p1)))) (Qmult g (Qpos (nR p2)))) h)) = Qmult (Qplus (Qplus (Qplus (Qmult (Qmult (a + c)%Z (Qpos p1)) (Qpos p2)) (Qmult (a + b + c + d)%Z (Qpos p1))) (Qmult c (Qpos p2))) (c + d)%Z) (Qinv (Qplus (Qplus (Qplus (Qmult (Qmult (e + g)%Z (Qpos p1)) (Qpos p2)) (Qmult (e + f + g + h)%Z (Qpos p1))) (Qmult g (Qpos p2))) (g + h)%Z)).
proof: Proof. Proof spec_Qquadratic_Qpositive_to_Q_dL_nR. Lemma spec_Qquadratic_Qpositive_to_Q_dL_dL : 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 (dL p1) (dL p2) = spec_Qquadratic_Qpositive_to_Q (a + b + c + d) (b + d) (c + d) d (e + f + g + h) (f + h) (g + h) h p1 p2. Proof. abstract (intros a b c d e f g h p1 p2; unfold spec_Qquadratic_Qpositive_to_Q at 1 in |- *; rewrite Qdiv_num_denom with (p := Qmult (Qplus (Qpos p1) Qone) (Qplus (Qpos p2) Qone)); [ idtac | discriminate ]; unfold spec_Qquadratic_Qpositive_to_Q in |- *; repeat rewrite Z_to_Qplus; do 2 rewrite Qpos_dL; apply f_equal2 with Q Q; [ field | apply f_equal with Q; field ]; split; discriminate). Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)