proposition: Lemma coding_Q : forall (m n : Z) (Hdenom : n <> 0%Z), fraction_encoding m n Hdenom = spec_fraction_encoding m n.
proof: Proof. intros m n Hdenom; unfold spec_fraction_encoding in |- *. functional induction (fraction_encoding m n Hdenom). set (x := Qinv n) in *. set (y := Z_to_Q m) in *. assert (x = Qinv n); trivial. assert (y = m); trivial. generalize H H0. clear H H0 e . functional induction (Qmult y x); intros. apply False_ind. apply (Zorder.Zlt_not_eq _ _ l). rewrite <- Zsgn_15. apply Zsgn_6. rewrite Z_eq_mult; try reflexivity. apply eq_Z_to_Q. symmetry in |- *; assumption. apply False_ind. apply Hdenom. apply eq_Z_to_Q. apply Qinv_0. symmetry in |- *; assumption. apply False_ind. apply (Zlt_asym _ _ l). rewrite <- Zsgn_15. apply Zsgn_26. assert (Hm : (0 < m)%Z); [ idtac | assert (Hn' : (0 < n)%Z); [ idtac | abstract auto with zarith ] ]. apply Qpos_POS_1 with x'. symmetry in |- *; assumption. apply pos_Z_to_Q. apply Qinv_1. rewrite <- H. abstract auto with *. apply f_equal with Qpositive. rewrite coding. unfold spec_positive_fraction_encoding in |- *. apply f_equal2 with Qpositive Qpositive. assert (Hm : (0 < m)%Z); [ apply Qpos_POS_1 with x'; symmetry in |- *; assumption | idtac ]. rewrite <- (Z_to_Qpositive_equal m (Z.abs m) Hm). apply Qpos_injective. rewrite <- Z_to_Qpositive_to_Q. symmetry in |- *; assumption. symmetry in |- *; apply Z.abs_eq; apply Zlt_le_weak; assumption. apply Qneg_injective. rewrite H. change (Qinv (Qneg (Z_to_Qpositive (Z.abs n) (Zabs_11 n Hdenom))) = Qinv n) in |- *. apply f_equal with Q. assert (Hn' : (n < 0)%Z); [ apply neg_Z_to_Q; apply Qinv_2; rewrite <- H; apply Qlt_neg_zero | idtac ]. destruct n as [| pn| pn]; try discriminate Hn'. unfold Z_to_Q in |- *. apply f_equal with Qpositive. reflexivity. apply False_ind. apply Hdenom. apply eq_Z_to_Q. apply Qinv_0. symmetry in |- *; assumption. apply f_equal with Qpositive. rewrite coding. unfold spec_positive_fraction_encoding in |- *. apply f_equal2 with Qpositive Qpositive. apply Qneg_injective. assert (Hm : (m < 0)%Z); [ apply neg_Z_to_Q; rewrite <- H0; apply Qlt_neg_zero | idtac ]. destruct m as [| pm| pm]; try discriminate Hm. rewrite H0. unfold Z_to_Q in |- *. apply f_equal with Qpositive. reflexivity. apply Qpos_injective. rewrite H. change (Qinv (Qpos (Z_to_Qpositive (Z.abs n) (Zabs_11 n Hdenom))) = Qinv n) in |- *. apply f_equal with Q. rewrite <- Z_to_Qpositive_to_Q. rewrite Z.abs_eq; try reflexivity. apply Zlt_le_weak. apply pos_Z_to_Q. apply Qinv_1. rewrite <- H. apply Qlt_zero_pos. apply False_ind. apply (Zlt_asym _ _ l). rewrite <- Zsgn_15. apply Zsgn_26. assert (Hm : (m < 0)%Z); [ idtac | assert (Hn' : (n < 0)%Z); [ idtac | abstract auto with zarith ] ]. apply Qneg_NEG_1 with x'. symmetry in |- *; assumption. apply neg_Z_to_Q. apply Qinv_2. rewrite <- H. apply Qlt_neg_zero. set (x := Qinv n) in *. set (y := Z_to_Q m) in *. assert (x = Qinv n); trivial. assert (y = m); trivial. generalize H H0. clear e H H0. functional induction (Qmult y x); intros. apply False_ind. generalize (Z.gt_lt _ _ g); clear g; intro z. apply (Zorder.Zlt_not_eq _ _ z). symmetry in |- *. rewrite <- Zsgn_15. apply Zsgn_6. rewrite Z_eq_mult; try reflexivity. apply eq_Z_to_Q. symmetry in |- *; assumption. apply False_ind. apply Hdenom. apply eq_Z_to_Q. apply Qinv_0. symmetry in |- *; assumption. apply f_equal with Qpositive. rewrite coding. unfold spec_positive_fraction_encoding in |- *. apply f_equal2 with Qpositive Qpositive. assert (Hm : (0 < m)%Z); [ apply Qpos_POS_1 with x'; symmetry in |- *; assumption | idtac ]. rewrite <- (Z_to_Qpositive_equal m (Z.abs m) Hm). apply Qpos_injective. rewrite <- Z_to_Qpositive_to_Q. symmetry in |- *; assumption. symmetry in |- *; apply Z.abs_eq; apply Zlt_le_weak; assumption. apply Qpos_injective. rewrite H. change (Qinv (Qpos (Z_to_Qpositive (Z.abs n) (Zabs_11 n Hdenom))) = Qinv n) in |- *. apply f_equal with Q. rewrite <- Z_to_Qpositive_to_Q. rewrite Z.abs_eq; try reflexivity. apply Zlt_le_weak. apply pos_Z_to_Q. apply Qinv_1. rewrite <- H. apply Qlt_zero_pos. apply False_ind. generalize (Z.gt_lt _ _ g); clear g; intro z. apply (Zlt_asym _ _ z). rewrite <- Zsgn_15. apply Zsgn_27. assert (Hm : (0 < m)%Z); [ idtac | assert (Hn' : (n < 0)%Z); [ idtac | try abstract auto with zarith ] ]. apply Qpos_POS_1 with x'. symmetry in |- *; assumption. apply neg_Z_to_Q. apply Qinv_2. rewrite <- H. abstract auto with *. apply False_ind. apply Hdenom. apply eq_Z_to_Q. apply Qinv_0. symmetry in |- *; assumption. apply False_ind. generalize (Z.gt_lt _ _ g); clear g; intro z. apply (Zlt_asym _ _ z). rewrite <- Zsgn_15. apply Zsgn_27. assert (Hm : (m < 0)%Z); [ idtac | assert (Hn' : (0 < n)%Z); [ idtac | abstract auto with zarith ] ]. apply Qneg_NEG_1 with x'. symmetry in |- *; assumption. apply pos_Z_to_Q. apply Qinv_1. rewrite <- H. apply Qlt_zero_pos. apply f_equal with Qpositive. rewrite coding. unfold spec_positive_fraction_encoding in |- *. apply f_equal2 with Qpositive Qpositive. apply Qneg_injective. assert (Hm : (m < 0)%Z); [ apply neg_Z_to_Q; rewrite <- H0; apply Qlt_neg_zero | idtac ]. destruct m as [| pm| pm]; try discriminate Hm. rewrite H0. unfold Z_to_Q in |- *. apply f_equal with Qpositive. reflexivity. apply Qneg_injective. rewrite H. change (Qinv (Qneg (Z_to_Qpositive (Z.abs n) (Zabs_11 n Hdenom))) = Qinv n) in |- *. apply f_equal with Q. assert (Hn' : (n < 0)%Z); [ apply neg_Z_to_Q; apply Qinv_2; rewrite <- H; apply Qlt_neg_zero | idtac ]. destruct n as [| pn| pn]; try discriminate Hn'. unfold Z_to_Q in |- *. apply f_equal with Qpositive. reflexivity. replace m with 0%Z. reflexivity. symmetry in |- *; apply Zmult_integral_l with n; [ idtac | apply Zsgn_2; rewrite Zsgn_15 ]; assumption. Defined.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)