fact: Fixpoint Qhomographic_Qpositive_to_Qpositive (a b c d : Z) (p : Qpositive) (hyp : homographicAcc a b c d p) {struct hyp} : Qpositive := match Qpositive_dec_One p with | left H_p_is_One => let H := eq_ind p (fun p : Qpositive => homographicAcc a b c d p) hyp One H_p_is_One in (fun hyp0 : homographicAcc a b c d One => (fun (Hab : (0 < a + b)%Z) (Hcd : (0 < c + d)%Z) => positive_fraction_encoding (a + b) (c + d) Hab Hcd) (homographicacc_0_num a b c d hyp0) (homographicacc_0_denom a b c d hyp0)) H | right H_p_not_One => match top_more_informative a b c d with | left H_abcd => nR (Qhomographic_Qpositive_to_Qpositive (a - c)%Z (b - d)%Z c d p (homographicacc_1 a b c d p hyp H_p_not_One H_abcd)) | right H_abcd => match top_more_informative c d a b with | left H_cdab => dL (Qhomographic_Qpositive_to_Qpositive a b (c - a)%Z (d - b)%Z p (homographicacc_2 a b c d p hyp H_p_not_One H_abcd H_cdab)) | right H_cdab => match p as q return (p = q -> Qpositive) with | nR q => fun H : p = nR q => Qhomographic_Qpositive_to_Qpositive a (a + b)%Z c (c + d)%Z q (homographicacc_3 a b c d p hyp q H H_abcd H_cdab) | dL q => fun H : p = dL q => Qhomographic_Qpositive_to_Qpositive (a + b)%Z b (c + d)%Z d q (homographicacc_3' a b c d p hyp q H H_abcd H_cdab) | One => fun q : p = One => False_rec Qpositive (False_ind False (H_p_not_One q)) end (refl_equal p) end end end.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)