proposition: Lemma spec_ni2_nR_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 (a - c)%Z (Qpos q)) (b - d)%Z) -> nR (spec_ni2 (a - c) (b - d) c d 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_nR_does. unfold spec_ni2 in |- *. 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. apply f_equal with Q. repeat rewrite Z_to_Qminus. abstract (field; assumption). apply Qlt_mult_pos_pos; try apply Qinv_pos; assumption. apply Qlt_zero_one. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)