proposition: Lemma positive_fraction_encoding_0 : forall (m n : Z) (Hm : (0 < m)%Z) (Hn : (0 < n)%Z), m = n -> positive_fraction_encoding m n Hm Hn = One.
proof: Proof. intros. unfold positive_fraction_encoding in |- *. apply encoding_algorithm_0. assumption. Defined.
imports: Coq(ZArithRing) Coq(FunInd)