proposition: Lemma encoding_algorithm_1 : forall (m n : Z) (Hm : (0 < m)%Z) (Hn : (0 < n)%Z) (H : fractionalAcc m n), (m < n)%Z -> forall (H'm : (0 < m)%Z) (H'nm : (0 < n - m)%Z) (H' : fractionalAcc m (n - m)), encoding_algorithm m n Hm Hn H = dL (encoding_algorithm m (n - m) H'm H'nm H').
proof: Proof. intros. apply trans_eq with (encoding_algorithm m n Hm Hn (fractionalacc1 m n Hm 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)