proposition: Lemma spec_Qquadratic_Qpositive_to_Qpositive2_nR_dL : forall (a b c d e f g h : Z) (p1 p2 : Qpositive), Qplus (Qplus (Qplus (Qmult (Qmult (Qplus a b) (Qpos p1)) (Qpos p2)) (Qmult b (Qpos p1))) (Qmult (Qplus (Qplus (Qplus a b) c) d) (Qpos p2))) (Qplus b d) <> Zero -> Qplus (Qplus (Qplus (Qmult (Qmult (Qplus e f) (Qpos p1)) (Qpos p2)) (Qmult f (Qpos p1))) (Qmult (Qplus (Qplus (Qplus e f) g) h) (Qpos p2))) (Qplus f h) <> Zero -> spec_Qquadratic_Qpositive_to_Qpositive2 a b c d e f g h (nR p1) (dL p2) = spec_Qquadratic_Qpositive_to_Qpositive2 (a + b) b (a + b + c + d) (b + d) (e + f) f (e + f + g + h) (f + h) p1 p2.
proof: Proof. abstract (intros a b c d e f g h p1 p2 H_num H_denom; unfold spec_Qquadratic_Qpositive_to_Qpositive2 at 1 in |- *; rewrite <- Q_tail_Qinv; rewrite <- Q_tail_Qmult; rewrite Qpos_nR; rewrite Qpos_dL; [ idtac | intro H; apply (Qmult_resp_nonzero _ (Qinv (Qplus (Qpos p2) Qone)) H_num); [ discriminate | rewrite <- H; field; discriminate ] | apply Qinv_resp_nonzero; intro H; apply (Qmult_resp_nonzero _ (Qinv (Qplus (Qpos p2) Qone)) H_denom); [ discriminate | rewrite <- H; field; discriminate ] ]; rewrite Qdiv_num_denom with (p := Qplus (Qpos p2) Qone); [ idtac | discriminate ]; unfold spec_Qquadratic_Qpositive_to_Qpositive2 in |- *; repeat rewrite Z_to_Qplus; rewrite <- Q_tail_Qinv; rewrite <- Q_tail_Qmult; [ idtac | assumption | apply Qinv_resp_nonzero; assumption ]; apply f_equal with Q; apply f_equal2 with Q Q; [ field | apply f_equal with Q; field ]; discriminate). Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)