proposition: Lemma positive_fraction_encoding_equal : forall (a b : Z) (Ha1 Ha2 : (0 < a)%Z) (Hb1 Hb2 : (0 < b)%Z), positive_fraction_encoding a b Ha1 Hb1 = positive_fraction_encoding a b Ha2 Hb2.
proof: Proof. intros. unfold positive_fraction_encoding in |- *. apply encoding_algorithm_equal. Defined.
imports: Coq(ZArithRing) Coq(FunInd)