proposition: Lemma spec_Qquadratic_Qpositive_to_Qpositive2_dL_emission : forall (a b c d e f g h : Z) (p1 p2 : Qpositive), 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) -> Qlt Zero (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) -> dL (spec_Qquadratic_Qpositive_to_Qpositive2 a b c d (e - a) (f - b) (g - c) (h - d) p1 p2) = spec_Qquadratic_Qpositive_to_Qpositive2 a b c d e f g h p1 p2.
proof: Proof. intros a b c d e f g h p1 p2 Habcd Hefgh Habcdefgh; generalize (Qlt_not_eq _ _ Habcd) (Qlt_not_eq _ _ Hefgh) (Qlt_not_eq _ _ Habcdefgh); intros Habcd' Hefgh' Habcdefgh'. rewrite what_dL_does. unfold spec_Qquadratic_Qpositive_to_Qpositive2 in |- *. repeat rewrite <- Q_tail_Qinv. repeat rewrite <- Q_tail_Qmult; match goal with | |- (Qinv _ <> _) => apply Qinv_resp_nonzero | |- _ => idtac end; try assumption. replace One with (Q_tail Qone); trivial. rewrite <- Q_tail_Qplus_pos; [ idtac | apply Qlt_mult_pos_pos; try apply Qinv_pos; assumption | apply Qlt_zero_one ]. rewrite <- Q_tail_Qinv. repeat rewrite <- Q_tail_Qmult; repeat match goal with | |- (Qinv _ <> _) => apply Qinv_resp_nonzero | |- (Qmult _ _ <> _) => apply Qmult_resp_nonzero end; [ idtac | assumption | assumption | apply Qlt_not_eq; apply Qlt_plus_pos_pos; [ apply Qlt_mult_pos_pos; try apply Qinv_pos; assumption | apply Qlt_zero_one ] ]. apply f_equal with Q. repeat rewrite Z_to_Qminus. repeat rewrite Z_to_Qminus in Habcdefgh'. replace (Qplus (Qmult (Qplus (Qplus (Qplus (Qmult (Qmult a (Qpos p1)) (Qpos p2)) (Qmult b (Qpos p1))) (Qmult c (Qpos p2))) d) (Qinv (Qplus (Qplus (Qplus (Qmult (Qmult (Qminus e a) (Qpos p1)) (Qpos p2)) (Qmult (Qminus f b) (Qpos p1))) (Qmult (Qminus g c) (Qpos p2))) (Qminus h d)))) Qone) with (Qmult (Qplus (Qplus (Qplus (Qmult (Qmult e (Qpos p1)) (Qpos p2)) (Qmult f (Qpos p1))) (Qmult g (Qpos p2))) h) (Qinv (Qplus (Qplus (Qplus (Qmult (Qmult (Qminus e a) (Qpos p1)) (Qpos p2)) (Qmult (Qminus f b) (Qpos p1))) (Qmult (Qminus g c) (Qpos p2))) (Qminus h d)))). symmetry in |- *. apply Qdiv_num_denom. apply Qinv_resp_nonzero. assumption. abstract (field; repeat rewrite Z_to_Qminus in Habcdefgh'; assumption). Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)