proposition: Lemma encoding_algorithm_equal : forall (a b : Z) (Ha1 Ha2 : (0 < a)%Z) (Hb1 Hb2 : (0 < b)%Z) (H1 H2 : fractionalAcc a b), encoding_algorithm a b Ha1 Hb1 H1 = encoding_algorithm a b Ha2 Hb2 H2.
proof: Proof. intros a b Ha1 Ha2 Hb1 Hb2 H1 H2. generalize Ha1 Hb1 Ha2 Hb2 H2. clear Ha1 Hb1 Ha2 Hb2 H2. pattern a, b, H1 in |- *. elim H1 using fractionalAcc_ind_dep. intros m n e Ha3 Hb3 Ha4 Hb4 H3; generalize e Ha3 Hb3 Ha4 Hb4; clear e Ha3 Hb3 Ha4 Hb4; pattern m, n, H3 in |- *; elim H3 using fractionalAcc_ind_dep. intros; simpl in |- *; case (Z_dec' m0 n0); [ intros [H_falsum| H_falsum]; Irreflex | trivial ]. intros; Irreflex. intros; Irreflex. intros m n z z0 H1' H_ind Ha3 Hb3 Ha4 Hb4 H3. generalize z z0 H1' H_ind Ha3 Hb3 Ha4 Hb4. clear a b H1 z z0 H_ind H1' Ha3 Hb3 Ha4 Hb4. pattern m, n, H3 in |- *. elim H3 using fractionalAcc_ind_dep. intros; Irreflex. intros; simpl in |- *; case (Z_dec' m0 n0); [ intros [H11| H_falsum] | trivial ]; [ apply f_equal with Qpositive; apply H_ind | Irreflex ]. intros; simpl in |- *; case (Z_dec' m0 n0); [ intros [H11| H_falsum] | trivial ]; [ apply f_equal with Qpositive; apply H_ind | Irreflex ]. intros m n z z0 H1' H_ind Ha3 Hb3 Ha4 Hb4 H3. generalize z z0 H1' H_ind Ha3 Hb3 Ha4 Hb4. clear a b H1 z z0 H_ind H1' Ha3 Hb3 Ha4 Hb4. pattern m, n, H3 in |- *. elim H3 using fractionalAcc_ind_dep. intros; Irreflex. intros; simpl in |- *; case (Z_dec' m0 n0); [ intros [H_falsum| H11] | trivial ]; [ Irreflex | apply f_equal with Qpositive; apply H_ind ]. intros; simpl in |- *; case (Z_dec' m0 n0); [ intros [H_falsum| H11] | trivial ]; [ Irreflex | apply f_equal with Qpositive; apply H_ind ]. Defined.
imports: Coq(ZArithRing) Coq(FunInd)