proposition: Lemma spec_ni2_dL_emission : forall (a b c d : Z) (q : Qpositive), Qlt Zero (Qplus (Qmult a (Qpos q)) b) -> Qlt Zero (Qplus (Qmult c (Qpos q)) d) -> Qlt Zero (Qplus (Qmult (c - a)%Z (Qpos q)) (d - b)%Z) -> dL (spec_ni2 a b (c - a) (d - b) q) = spec_ni2 a b c d q.
proof: Proof. intros a b c d q Hab Hcd Habcd; generalize (Qlt_not_eq _ _ Hab) (Qlt_not_eq _ _ Hcd) (Qlt_not_eq _ _ Habcd); intros Hab' Hcd' Habcd'. rewrite what_dL_does. unfold spec_ni2 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. rewrite <- Q_tail_Qinv. repeat rewrite <- Q_tail_Qmult; repeat match goal with | |- (Qinv _ <> _) => apply Qinv_resp_nonzero | |- (Qmult _ _ <> _) => apply Qmult_resp_nonzero end; try assumption. apply f_equal with Q. repeat rewrite Z_to_Qminus. Opaque Qmult Qplus Qinv Qone. field. repeat match goal with | |- (Qinv _ <> _) => apply Qinv_resp_nonzero | |- (Qmult _ _ <> _) => apply Qmult_resp_nonzero | |- (Qplus _ _ <> _) => do 2 rewrite Z_to_Qminus in Habcd'; assumption end; try assumption. split. apply Qlt_not_eq; trivial. do 2 rewrite Z_to_Qminus in Habcd'; assumption. apply Qlt_not_eq; apply Qlt_plus_pos_pos. apply Qlt_mult_pos_pos; try assumption. apply Qinv_pos; assumption. apply Qlt_zero_one. apply Qlt_mult_pos_pos; try apply Qinv_pos; assumption. apply Qlt_zero_one. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)