proposition: Lemma quadraticAcc_positive : forall (a b c d e f g h : Z) (p1 p2 : Qpositive), quadraticAcc a b c d e f g h p1 p2 -> Qlt Zero (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos p1)) (Qpos p2)) (Qmult b (Qpos p1))) (Qmult c (Qpos p2))) d) /\ Qlt Zero (Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos p1)) (Qpos p2)) (Qmult f (Qpos p1))) (Qmult g (Qpos p2))) h).
proof: Proof. intros a b c d e f g h p1 p2 H. induction H; try match goal with | id1:(_ /\ _) |- _ => elim id1; clear id1; intros IHrec1 IHrec2 end. rewrite H; repeat rewrite Qmult_one_right; replace (Qplus (Qplus (Qplus (Qmult a (Qpos p2)) b) (Qmult c (Qpos p2))) d) with (Qplus (Qmult (a + c)%Z (Qpos p2)) (b + d)%Z); [ replace (Qplus (Qplus (Qplus (Qmult e (Qpos p2)) f) (Qmult g (Qpos p2))) h) with (Qplus (Qmult (e + g)%Z (Qpos p2)) (f + h)%Z); [ apply homographicAcc_positive; assumption | idtac ] | idtac ]; repeat rewrite Z_to_Qplus; ring. rewrite H0; repeat rewrite Qmult_one_right; replace (Qplus (Qplus (Qplus (Qmult a (Qpos p1)) (Qmult b (Qpos p1))) c) d) with (Qplus (Qmult (a + b)%Z (Qpos p1)) (c + d)%Z); [ replace (Qplus (Qplus (Qplus (Qmult e (Qpos p1)) (Qmult f (Qpos p1))) g) h) with (Qplus (Qmult (e + f)%Z (Qpos p1)) (g + h)%Z); [ apply homographicAcc_positive; assumption | idtac ] | idtac ]; repeat rewrite Z_to_Qplus; ring. split; try assumption; replace a with (a - e + e)%Z; [ idtac | abstract auto with zarith ]; replace b with (b - f + f)%Z; [ idtac | abstract auto with zarith ]; replace c with (c - g + g)%Z; [ idtac | abstract auto with zarith ]; replace d with (d - h + h)%Z; [ idtac | abstract auto with zarith ]; repeat rewrite Z_to_Qplus; replace (Qplus (Qplus (Qplus (Qmult (Qmult (Qplus (a - e)%Z e) (Qpos p1)) (Qpos p2)) (Qmult (Qplus (b - f)%Z f) (Qpos p1))) (Qmult (Qplus (c - g)%Z g) (Qpos p2))) (Qplus (d - h)%Z h)) with (Qplus (Qplus (Qplus (Qplus (Qmult (Qmult (a - e)%Z (Qpos p1)) (Qpos p2)) (Qmult (b - f)%Z (Qpos p1))) (Qmult (c - g)%Z (Qpos p2))) (d - h)%Z) (Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos p1)) (Qpos p2)) (Qmult f (Qpos p1))) (Qmult g (Qpos p2))) h)); [ idtac | abstract ring ]; apply Qlt_plus_pos_pos; assumption. split; try assumption; replace e with (e - a + a)%Z; [ idtac | abstract auto with zarith ]; replace f with (f - b + b)%Z; [ idtac | abstract auto with zarith ]; replace g with (g - c + c)%Z; [ idtac | abstract auto with zarith ]; replace h with (h - d + d)%Z; [ idtac | abstract auto with zarith ]; repeat rewrite Z_to_Qplus; replace (Qplus (Qplus (Qplus (Qmult (Qmult (Qplus (e - a)%Z a) (Qpos p1)) (Qpos p2)) (Qmult (Qplus (f - b)%Z b) (Qpos p1))) (Qmult (Qplus (g - c)%Z c) (Qpos p2))) (Qplus (h - d)%Z d)) with (Qplus (Qplus (Qplus (Qplus (Qmult (Qmult (e - a)%Z (Qpos p1)) (Qpos p2)) (Qmult (f - b)%Z (Qpos p1))) (Qmult (g - c)%Z (Qpos p2))) (h - d)%Z) (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos p1)) (Qpos p2)) (Qmult b (Qpos p1))) (Qmult c (Qpos p2))) d)); [ idtac | abstract ring ]; apply Qlt_plus_pos_pos; assumption. repeat rewrite Qpos_nR; replace (Qplus (Qplus (Qplus (Qmult (Qmult a (Qplus (Qpos xs) Qone)) (Qplus (Qpos ys) Qone)) (Qmult b (Qplus (Qpos xs) Qone))) (Qmult c (Qplus (Qpos ys) Qone))) d) with (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos xs)) (Qpos ys)) (Qmult (a + b)%Z (Qpos xs))) (Qmult (a + c)%Z (Qpos ys))) (a + b + c + d)%Z); [ idtac | repeat rewrite Z_to_Qplus; abstract ring ]; replace (Qplus (Qplus (Qplus (Qmult (Qmult e (Qplus (Qpos xs) Qone)) (Qplus (Qpos ys) Qone)) (Qmult f (Qplus (Qpos xs) Qone))) (Qmult g (Qplus (Qpos ys) Qone))) h) with (Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos xs)) (Qpos ys)) (Qmult (e + f)%Z (Qpos xs))) (Qmult (e + g)%Z (Qpos ys))) (e + f + g + h)%Z); [ idtac | repeat rewrite Z_to_Qplus; abstract ring ]; split; assumption. abstract (repeat rewrite Qpos_nR; repeat rewrite Qpos_dL; replace (Qplus (Qplus (Qplus (Qmult (Qmult a (Qplus (Qpos xs) Qone)) (Qmult (Qpos ys) (Qinv (Qplus (Qpos ys) Qone)))) (Qmult b (Qplus (Qpos xs) Qone))) (Qmult c (Qmult (Qpos ys) (Qinv (Qplus (Qpos ys) Qone))))) d) with (Qmult (Qplus (Qplus (Qplus (Qmult (Qmult (a + b)%Z (Qpos xs)) (Qpos ys)) (Qmult b (Qpos xs))) (Qmult (a + b + c + d)%Z (Qpos ys))) (b + d)%Z) (Qinv (Qplus (Qpos ys) Qone))); [ idtac | repeat rewrite Z_to_Qplus; abstract (field; discriminate) ]; replace (Qplus (Qplus (Qplus (Qmult (Qmult e (Qplus (Qpos xs) Qone)) (Qmult (Qpos ys) (Qinv (Qplus (Qpos ys) Qone)))) (Qmult f (Qplus (Qpos xs) Qone))) (Qmult g (Qmult (Qpos ys) (Qinv (Qplus (Qpos ys) Qone))))) h) with (Qmult (Qplus (Qplus (Qplus (Qmult (Qmult (e + f)%Z (Qpos xs)) (Qpos ys)) (Qmult f (Qpos xs))) (Qmult (e + f + g + h)%Z (Qpos ys))) (f + h)%Z) (Qinv (Qplus (Qpos ys) Qone))); [ idtac | repeat rewrite Z_to_Qplus; abstract (field; discriminate) ]; split; apply Qlt_mult_pos_pos; try assumption; apply Qinv_pos; apply Qlt_plus_pos_pos; abstract auto with *). abstract (repeat rewrite Qpos_nR; repeat rewrite Qpos_dL; replace (Qplus (Qplus (Qplus (Qmult (Qmult a (Qmult (Qpos xs) (Qinv (Qplus (Qpos xs) Qone)))) (Qplus (Qpos ys) Qone)) (Qmult b (Qmult (Qpos xs) (Qinv (Qplus (Qpos xs) Qone))))) (Qmult c (Qplus (Qpos ys) Qone))) d) with (Qmult (Qplus (Qplus (Qplus (Qmult (Qmult (a + c)%Z (Qpos xs)) (Qpos ys)) (Qmult (a + b + c + d)%Z (Qpos xs))) (Qmult c (Qpos ys))) (c + d)%Z) (Qinv (Qplus (Qpos xs) Qone))); [ idtac | repeat rewrite Z_to_Qplus; abstract (field; discriminate) ]; replace (Qplus (Qplus (Qplus (Qmult (Qmult e (Qmult (Qpos xs) (Qinv (Qplus (Qpos xs) Qone)))) (Qplus (Qpos ys) Qone)) (Qmult f (Qmult (Qpos xs) (Qinv (Qplus (Qpos xs) Qone))))) (Qmult g (Qplus (Qpos ys) Qone))) h) with (Qmult (Qplus (Qplus (Qplus (Qmult (Qmult (e + g)%Z (Qpos xs)) (Qpos ys)) (Qmult (e + f + g + h)%Z (Qpos xs))) (Qmult g (Qpos ys))) (g + h)%Z) (Qinv (Qplus (Qpos xs) Qone))); [ idtac | repeat rewrite Z_to_Qplus; abstract (field; discriminate) ]; split; apply Qlt_mult_pos_pos; try assumption; apply Qinv_pos; apply Qlt_plus_pos_pos; abstract auto with *). abstract (repeat rewrite Qpos_dL; replace (Qplus (Qplus (Qplus (Qmult (Qmult a (Qmult (Qpos xs) (Qinv (Qplus (Qpos xs) Qone)))) (Qmult (Qpos ys) (Qinv (Qplus (Qpos ys) Qone)))) (Qmult b (Qmult (Qpos xs) (Qinv (Qplus (Qpos xs) Qone))))) (Qmult c (Qmult (Qpos ys) (Qinv (Qplus (Qpos ys) Qone))))) d) with (Qmult (Qplus (Qplus (Qplus (Qmult (Qmult (a + b + c + d)%Z (Qpos xs)) (Qpos ys)) (Qmult (b + d)%Z (Qpos xs))) (Qmult (c + d)%Z (Qpos ys))) d) (Qinv (Qmult (Qplus (Qpos xs) Qone) (Qplus (Qpos ys) Qone)))); [ idtac | repeat rewrite Z_to_Qplus; field; split; discriminate ]; replace (Qplus (Qplus (Qplus (Qmult (Qmult e (Qmult (Qpos xs) (Qinv (Qplus (Qpos xs) Qone)))) (Qmult (Qpos ys) (Qinv (Qplus (Qpos ys) Qone)))) (Qmult f (Qmult (Qpos xs) (Qinv (Qplus (Qpos xs) Qone))))) (Qmult g (Qmult (Qpos ys) (Qinv (Qplus (Qpos ys) Qone))))) h) with (Qmult (Qplus (Qplus (Qplus (Qmult (Qmult (e + f + g + h)%Z (Qpos xs)) (Qpos ys)) (Qmult (f + h)%Z (Qpos xs))) (Qmult (g + h)%Z (Qpos ys))) h) (Qinv (Qmult (Qplus (Qpos xs) Qone) (Qplus (Qpos ys) Qone)))); [ idtac | repeat rewrite Z_to_Qplus; field; split; discriminate ]; split; apply Qlt_mult_pos_pos; try assumption; apply Qinv_pos; apply Qlt_mult_pos_pos; apply Qlt_plus_pos_pos; abstract auto with *). Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)