proposition: Lemma spec_Qquadratic_Qpositive_to_Q_nR_dL_unfolded : forall (a b c d e f g h : Z) (p1 p2 : Qpositive), Qmult (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos (nR p1))) (Qpos (dL p2))) (Qmult b (Qpos (nR p1)))) (Qmult c (Qpos (dL p2)))) d) (Qinv (Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos (nR p1))) (Qpos (dL p2))) (Qmult f (Qpos (nR p1)))) (Qmult g (Qpos (dL p2)))) h)) = Qmult (Qplus (Qplus (Qplus (Qmult (Qmult (a + b)%Z (Qpos p1)) (Qpos p2)) (Qmult b (Qpos p1))) (Qmult (a + b + c + d)%Z (Qpos p2))) (b + d)%Z) (Qinv (Qplus (Qplus (Qplus (Qmult (Qmult (e + f)%Z (Qpos p1)) (Qpos p2)) (Qmult f (Qpos p1))) (Qmult (e + f + g + h)%Z (Qpos p2))) (f + h)%Z)).
proof: Proof. Proof spec_Qquadratic_Qpositive_to_Q_nR_dL. Lemma spec_Qquadratic_Qpositive_to_Q_dL_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 (dL p1) (nR p2) = spec_Qquadratic_Qpositive_to_Q (a + c) (a + b + c + d) c (c + d) (e + g) (e + f + g + h) g (g + h) p1 p2. Proof. abstract (intros a b c d e f g h p1 p2; rewrite spec_Qquadratic_Qpositive_to_Q_commut; rewrite spec_Qquadratic_Qpositive_to_Q_nR_dL; rewrite spec_Qquadratic_Qpositive_to_Q_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)