proposition: Lemma Qhomographic_Qpositive_to_Qpositive_2 : forall (a b c d : Z) (p : Qpositive) (hyp : homographicAcc a b c d p), p <> One -> ~ top_more a b c d -> top_more c d a b -> forall h : homographicAcc a b (c - a) (d - b) p, Qhomographic_Qpositive_to_Qpositive a b c d p hyp = dL (Qhomographic_Qpositive_to_Qpositive a b (c - a) (d - b) p h).
proof: Proof. intros. apply trans_eq with (Qhomographic_Qpositive_to_Qpositive a b c d p (homographicacc2 a b c d p H H0 H1 h)). apply Qhomographic_Qpositive_to_Qpositive_equal. simpl in |- *. case (Qpositive_dec_One p); intros Hp; [ Falsum | idtac ]. case (top_more_informative a b c d); intros Habcd; [ Falsum | idtac ]. case (top_more_informative c d a b); intros Hcdab; [ idtac | Falsum ]. apply f_equal with Qpositive; reflexivity. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)