proposition: Lemma spec_Qquadratic_Qpositive_to_Qpositive2_dL_nR : forall (a b c d e f g h : Z) (p1 p2 : Qpositive), Qplus (Qplus (Qplus (Qmult (Qmult (Qplus a c) (Qpos p1)) (Qpos p2)) (Qmult (Qplus (Qplus (Qplus a b) c) d) (Qpos p1))) (Qmult c (Qpos p2))) (Qplus c d) <> Zero -> Qplus (Qplus (Qplus (Qmult (Qmult (Qplus e g) (Qpos p1)) (Qpos p2)) (Qmult (Qplus (Qplus (Qplus e f) g) h) (Qpos p1))) (Qmult g (Qpos p2))) (Qplus g h) <> Zero -> spec_Qquadratic_Qpositive_to_Qpositive2 a b c d e f g h (dL p1) (nR p2) = spec_Qquadratic_Qpositive_to_Qpositive2 (a + c) (a + b + c + d) c (c + d) (e + g) (e + f + g + h) g (g + h) p1 p2.
proof: Proof. intros a b c d e f g h p1 p2 H_num H_denom; rewrite spec_Qquadratic_Qpositive_to_Qpositive2_commut; rewrite spec_Qquadratic_Qpositive_to_Qpositive2_nR_dL; [ idtac | intro H; apply H_num; rewrite <- H; ring | intro H; apply H_denom; rewrite <- H; ring ]; rewrite spec_Qquadratic_Qpositive_to_Qpositive2_commut; replace (a + b + c + d)%Z with (a + c + b + d)%Z; [ replace (e + f + g + h)%Z with (e + g + f + h)%Z; [ reflexivity | ring ] | ring ]. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)