proposition: Lemma encoding_algorithm_equal_strong : forall (a1 a2 b1 b2 : Z) (Ha1 : (0 < a1)%Z) (Ha2 : (0 < a2)%Z) (Hb1 : (0 < b1)%Z) (Hb2 : (0 < b2)%Z) (H1 : fractionalAcc a1 b1) (H2 : fractionalAcc a2 b2), a1 = a2 -> b1 = b2 -> encoding_algorithm a1 b1 Ha1 Hb1 H1 = encoding_algorithm a2 b2 Ha2 Hb2 H2.
proof: Proof. intros; subst; apply encoding_algorithm_equal. Defined.
imports: Coq(ZArithRing) Coq(FunInd)