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