proposition: Lemma output_bit : forall (a b c d : Z) (p : Qpositive) (hyp_Acc : homographicAcc a b c d p), Qhomographic_Qpositive_to_Qpositive a b c d p hyp_Acc = spec_ni2 a b c d p.
proof: Proof. intros a b c d p hyp_Acc. generalize (homographicAcc_positive_numerator _ _ _ _ _ hyp_Acc). generalize (homographicAcc_positive_denominator _ _ _ _ _ hyp_Acc). pattern a, b, c, d, p, hyp_Acc in |- *. elim hyp_Acc using homographicAcc_ind_dep; clear a b c d p hyp_Acc; intros; simpl in |- *. unfold spec_ni2 in |- *; case (Qpositive_dec_One p); intros Hp; [ idtac | Falsum ]; rewrite coding; unfold spec_positive_fraction_encoding in |- *; replace (Qpos p) with Qone; [ idtac | rewrite e; trivial ]; repeat rewrite Qmult_one_right; repeat rewrite <- Z_to_Qplus; repeat rewrite Z_to_Qpositive_Q_tail_pos; reflexivity. case (Qpositive_dec_One p); intros Hp; [ Falsum | idtac ]; case (top_more_informative a b c d); intros Habcd; [ idtac | Falsum ]; generalize (homographicAcc_positive_numerator _ _ _ _ _ h); intros H_acpbd; rewrite H; trivial; apply spec_ni2_nR_emission; assumption. 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 ]; generalize (homographicAcc_positive_denominator _ _ _ _ _ h); intros H_acpbd; rewrite H; trivial; apply spec_ni2_dL_emission; assumption. case (top_more_informative a b c d); intros Habcd; [ Falsum | idtac ]; case (top_more_informative c d a b); intros Hcdab; [ Falsum | idtac ]; generalize (homographicAcc_positive_numerator _ _ _ _ _ h); generalize (homographicAcc_positive_denominator _ _ _ _ _ h); intros H_acpbd H_acpbd'; rewrite H; trivial; rewrite spec_ni2_nR; reflexivity. case (top_more_informative a b c d); intros Habcd; [ Falsum | idtac ]; case (top_more_informative c d a b); intros Hcdab; [ Falsum | idtac ]; generalize (homographicAcc_positive_numerator _ _ _ _ _ h); generalize (homographicAcc_positive_denominator _ _ _ _ _ h); intros H_acpbd H_acpbd'; rewrite H; trivial. rewrite spec_ni2_dL; reflexivity || apply Qlt_not_eq; assumption. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)