proposition: Lemma homographicAcc_positive : forall (a b c d : Z) (p : Qpositive), homographicAcc a b c d p -> Qlt Zero (Qplus (Qmult (Z_to_Q a) (Qpos p)) (Z_to_Q b)) /\ Qlt Zero (Qplus (Qmult (Z_to_Q c) (Qpos p)) (Z_to_Q d)).
proof: Proof. intros. induction H; try match goal with | id1:(_ /\ _) |- _ => elim id1; clear id1; intros IH_xind1 IH_ind2 end. split; rewrite H; rewrite Qmult_one_right; rewrite <- Z_to_Qplus; apply Z_to_Q_pos; assumption. split; try assumption; replace a with (a - c + c)%Z; try abstract auto with zarith; replace b with (b - d + d)%Z; try abstract auto with zarith; repeat rewrite Z_to_Qplus; replace (Qplus (Qmult (Qplus (a - c)%Z c) (Qpos p)) (Qplus (b - d)%Z d)) with (Qplus (Qplus (Qmult (a - c)%Z (Qpos p)) (b - d)%Z) (Qplus (Qmult c (Qpos p)) d)); try abstract ring; apply Qlt_plus_pos_pos; assumption. split; try assumption; replace c with (c - a + a)%Z; try abstract auto with zarith; replace d with (d - b + b)%Z; try abstract auto with zarith; repeat rewrite Z_to_Qplus; replace (Qplus (Qmult (Qplus (c - a)%Z a) (Qpos p)) (Qplus (d - b)%Z b)) with (Qplus (Qplus (Qmult (c - a)%Z (Qpos p)) (d - b)%Z) (Qplus (Qmult a (Qpos p)) b)); try abstract ring; apply Qlt_plus_pos_pos; assumption. split; rewrite Qmult_Z_nR; rewrite <- Qplus_assoc; rewrite <- Z_to_Qplus; assumption. split; rewrite Qmult_Z_plus_Z_dL; apply Qlt_mult_pos_pos; try assumption; apply Qinv_pos; abstract auto with *. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)