proposition: Lemma spec_Qquadratic_Qpositive_to_Qpositive2_nR_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 (a - e)%Z (Qpos p1)) (Qpos p2)) (Qmult (b - f)%Z (Qpos p1))) (Qmult (c - g)%Z (Qpos p2))) (d - h)%Z) -> nR (spec_Qquadratic_Qpositive_to_Qpositive2 (a - e) (b - f) (c - g) (d - h) e f g h 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_nR_does. unfold spec_Qquadratic_Qpositive_to_Qpositive2 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. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)