proposition: Lemma Qhomographic_Qpositive_to_Qpositive_3 : forall (a b c d : Z) (p : Qpositive) (hyp : homographicAcc a b c d p), ~ top_more a b c d -> ~ top_more c d a b -> forall xs : Qpositive, p = nR xs -> forall h : homographicAcc a (a + b) c (c + d) xs, Qhomographic_Qpositive_to_Qpositive a b c d p hyp = Qhomographic_Qpositive_to_Qpositive a (a + b) c (c + d) xs h.
proof: Proof. intros. apply trans_eq with (Qhomographic_Qpositive_to_Qpositive a b c d (nR xs) (homographicacc3 a b c d xs H H0 h)). apply Qhomographic_Qpositive_to_Qpositive_equal_strong; trivial. simpl in |- *. case (top_more_informative a b c d); intros Habcd; [ Falsum | idtac ]. case (top_more_informative c d a b); intros Hcdab; [ Falsum | idtac ]. reflexivity. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)