proposition: Lemma Qhomographic_Qpositive_to_Qpositive_equal : forall (a b c d : Z) (p : Qpositive) (hyp1 hyp2 : homographicAcc a b c d p), Qhomographic_Qpositive_to_Qpositive a b c d p hyp1 = Qhomographic_Qpositive_to_Qpositive a b c d p hyp2.
proof: Proof. intros a b c d p hyp1 hyp2. generalize hyp2. clear hyp2. pattern a, b, c, d, p, hyp1 in |- *. elim hyp1 using homographicAcc_ind_dep; clear a b c d p hyp1. intros a b c d p Hp Hab Hcd hyp2; generalize Hp Hab Hcd; clear Hp Hab Hcd. pattern a, b, c, d, p, hyp2 in |- *. elim hyp2 using homographicAcc_ind_dep; clear a b c d p hyp2; intros. simpl in |- *. case (Qpositive_dec_One p); intro Hp_; [ idtac | Falsum ]. apply positive_fraction_encoding_equal. Falsum. Falsum. discriminate Hp. discriminate Hp. intros a b c d p Hp Habcd hyp1 H_ind hyp2; generalize Hp Habcd hyp1 H_ind; clear Hp Habcd H_ind hyp1. pattern a, b, c, d, p, hyp2 in |- *. elim hyp2 using homographicAcc_ind_dep; clear a b c d p hyp2; intros. Falsum. simpl in |- *; case (Qpositive_dec_One p); intro Hp_; [ Falsum | idtac ]; case (top_more_informative a b c d); intro Habcd_; [ idtac | Falsum ]; apply f_equal with Qpositive; apply H_ind. Falsum. Falsum. Falsum. intros a b c d p Hp Habcd Hcdab hyp1 H_ind hyp2; generalize Hp Habcd Hcdab hyp1 H_ind; clear Hp Habcd Hcdab H_ind hyp1. pattern a, b, c, d, p, hyp2 in |- *. elim hyp2 using homographicAcc_ind_dep; clear a b c d p hyp2; intros. Falsum. Falsum. simpl in |- *; case (Qpositive_dec_One p); intro Hp_; [ Falsum | idtac ]; case (top_more_informative a b c d); intro Habcd_; [ Falsum | idtac ]; case (top_more_informative c d a b); intro Hcdab_; [ idtac | Falsum ]; apply f_equal with Qpositive; apply H_ind. Falsum. Falsum. intros a b c d xs Habcd Hcdab hyp1 H_ind hyp2. set (P := nR xs) in *; assert (HP : P = nR xs); trivial; generalize HP. generalize Habcd Hcdab hyp1 H_ind. clear Habcd Hcdab H_ind hyp1. elim hyp2 using homographicAcc_ind_dep with (P := fun (a b c d : Z) (P : Qpositive) (hyp2 : homographicAcc a b c d P) => forall (Habcd : ~ top_more a b c d) (Hcdab : ~ top_more c d a b) (hyp1 : homographicAcc a (a + b) c (c + d) xs), (forall hyp2 : homographicAcc a (a + b) c (c + d) xs, Qhomographic_Qpositive_to_Qpositive a (a + b) c (c + d) xs hyp1 = Qhomographic_Qpositive_to_Qpositive a (a + b) c (c + d) xs hyp2) -> P = nR xs -> Qhomographic_Qpositive_to_Qpositive a b c d (nR xs) (homographicacc3 a b c d xs Habcd Hcdab hyp1) = Qhomographic_Qpositive_to_Qpositive a b c d P hyp2); clear a b c d hyp2; intros. Falsum; rewrite H0 in e; discriminate e. Falsum. Falsum. simpl in |- *. case (top_more_informative a b c d); intro Habcd_; [ Falsum | idtac ]; case (top_more_informative c d a b); intro Hcdab_; [ Falsum | idtac ]. generalize h; let T_local := eval compute in (f_equal Qpositive_tail H1) in rewrite T_local. intro; apply H0. discriminate H1. intros a b c d xs Habcd Hcdab hyp1 H_ind hyp2. set (P := dL xs) in *; assert (HP : P = dL xs); trivial; generalize HP. generalize Habcd Hcdab hyp1 H_ind. clear Habcd Hcdab H_ind hyp1. elim hyp2 using homographicAcc_ind_dep with (P := fun (a b c d : Z) (P : Qpositive) (hyp2 : homographicAcc a b c d P) => forall (Habcd : ~ top_more a b c d) (Hcdab : ~ top_more c d a b) (hyp1 : homographicAcc (a + b) b (c + d) d xs), (forall hyp2 : homographicAcc (a + b) b (c + d) d xs, Qhomographic_Qpositive_to_Qpositive (a + b) b (c + d) d xs hyp1 = Qhomographic_Qpositive_to_Qpositive (a + b) b (c + d) d xs hyp2) -> P = dL xs -> Qhomographic_Qpositive_to_Qpositive a b c d (dL xs) (homographicacc3' a b c d xs Habcd Hcdab hyp1) = Qhomographic_Qpositive_to_Qpositive a b c d P hyp2); clear a b c d hyp2; intros. Falsum; rewrite H0 in e; discriminate e. Falsum. Falsum. discriminate H1. simpl in |- *. case (top_more_informative a b c d); intro Habcd_; [ Falsum | idtac ]; case (top_more_informative c d a b); intro Hcdab_; [ Falsum | idtac ]. generalize h; let T_local := eval compute in (f_equal Qpositive_tail H1) in rewrite T_local. intro; apply H0. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)