proposition: Lemma positive_fraction_encoding_1 : forall (m n : Z) (Hm : (0 < m)%Z) (Hn : (0 < n)%Z), (m < n)%Z -> forall (H'm : (0 < m)%Z) (H'nm : (0 < n - m)%Z), positive_fraction_encoding m n Hm Hn = dL (positive_fraction_encoding m (n - m) H'm H'nm).
proof: Proof. intros. unfold positive_fraction_encoding in |- *. apply encoding_algorithm_1. assumption. Defined.
imports: Coq(ZArithRing) Coq(FunInd)