proposition: Lemma homographicacc_3' : forall (a b c d : Z) (p : Qpositive), homographicAcc a b c d p -> forall xs : Qpositive, p = dL xs -> ~ top_more a b c d -> ~ top_more c d a b -> homographicAcc (a + b) b (c + d) d xs.
proof: Proof. intros a b c d p HAcc xs. case HAcc; intros; try solve [ Falsum ]; [ rewrite H2 in H; clear H2; discriminate H | discriminate H2 | let T_local := eval compute in (f_equal Qpositive_tail H2) in (rewrite <- T_local; assumption) ]. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)