proposition: Lemma encoding_algorithm_2 : forall (m n : Z) (Hm : (0 < m)%Z) (Hn : (0 < n)%Z) (H : fractionalAcc m n), (n < m)%Z -> forall (H'mn : (0 < m - n)%Z) (H'n : (0 < n)%Z) (H' : fractionalAcc (m - n) n), encoding_algorithm m n Hm Hn H = nR (encoding_algorithm (m - n) n H'mn H'n H').
proof: Proof. intros. apply trans_eq with (encoding_algorithm m n Hm Hn (fractionalacc2 m n Hn H0 H')). apply encoding_algorithm_equal. simpl in |- *; case (Z_dec' m n); [ intros [H_11| H_falsum] | intro H_falsum ]; Irreflex; apply f_equal with Qpositive; apply encoding_algorithm_equal. Defined.
imports: Coq(ZArithRing) Coq(FunInd)