proposition: Lemma Qhomographic_Qpositive_to_Qpositive_equal_strong : forall (a1 a2 b1 b2 c1 c2 d1 d2 : Z) (p1 p2 : Qpositive) (hyp1 : homographicAcc a1 b1 c1 d1 p1) (hyp2 : homographicAcc a2 b2 c2 d2 p2), a1 = a2 -> b1 = b2 -> c1 = c2 -> d1 = d2 -> p1 = p2 -> Qhomographic_Qpositive_to_Qpositive a1 b1 c1 d1 p1 hyp1 = Qhomographic_Qpositive_to_Qpositive a2 b2 c2 d2 p2 hyp2.
proof: Proof. intros. subst. apply Qhomographic_Qpositive_to_Qpositive_equal. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)