proposition: Lemma homographicacc_1 : forall (a b c d : Z) (p : Qpositive), homographicAcc a b c d p -> p <> One -> top_more a b c d -> homographicAcc (a - c) (b - d) c d p.
proof: Proof. simple destruct 1; intros; trivial; Falsum. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)