proposition: Lemma Qhomographic_Qpositive_to_Qpositive_1 : forall (a b c d : Z) (p : Qpositive) (hyp : homographicAcc a b c d p), p <> One -> top_more a b c d -> forall h : homographicAcc (a - c) (b - d) c d p, Qhomographic_Qpositive_to_Qpositive a b c d p hyp = nR (Qhomographic_Qpositive_to_Qpositive (a - c) (b - d) c d p h).
proof: Proof. intros. apply trans_eq with (Qhomographic_Qpositive_to_Qpositive a b c d p (homographicacc1 a b c d p H H0 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; [ idtac | Falsum ]. apply f_equal with Qpositive; reflexivity. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)