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