proposition: Lemma homographicacc_0_denom : forall a b c d : Z, homographicAcc a b c d One -> (0 < c + d)%Z.
proof: Proof. intros. abstract (inversion H; trivial; Irreflex; discriminate H0). Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)