Every strictly positive rational number can be obtained in a unique
manner by a succession of applications of functions N and D on
the number 1, where N and D are defined by the following
N(x) = 1 + x
D(x) = 1
1 + -
We can associate any strictly positive rational number to an element of
an inductive type with one constructor for one, and two other
constructors representing the functions N and D.
Define this inductive type.
Build the function that takes an
element of this type defined and returns
the numerator and denominator of the corresponding reduced fraction.
Note: this file solution contains also a proof
that the fraction we compute is irreducible. We admit Bezout's equality.
Notice that we use techniques described in
the chapter devoted to inductive predicates