proposition: Lemma positive_fraction_encoding_equal_strong : forall (a1 a2 b1 b2 : Z) (Ha1 : (0 < a1)%Z) (Ha2 : (0 < a2)%Z) (Hb1 : (0 < b1)%Z) (Hb2 : (0 < b2)%Z), a1 = a2 -> b1 = b2 -> positive_fraction_encoding a1 b1 Ha1 Hb1 = positive_fraction_encoding a2 b2 Ha2 Hb2.
proof: Proof. intros. unfold positive_fraction_encoding in |- *. apply encoding_algorithm_equal_strong. assumption. assumption. Defined.
imports: Coq(ZArithRing) Coq(FunInd)