# On fractions

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
equations:
N(x) = 1 + x
D(x) = 1
------
1
1 + -
x

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.

## Solution

This file

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

Going home

Pierre Castéran