proposition: Lemma homographicAcc_positive_denominator : forall (a b c d : Z) (p : Qpositive), homographicAcc a b c d p -> Qlt Zero (Qplus (Qmult (Z_to_Q c) (Qpos p)) (Z_to_Q d)).
proof: Proof. intros; elim (homographicAcc_positive _ _ _ _ _ H); trivial. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)