fact: Fixpoint rat_to_frac (r: rational) : nat * nat := match r with | One => (1, 1) | N x => let: (a, b) := rat_to_frac x in (b + a, b) | D x => let (a, b) := rat_to_frac x in (a, a + b) end.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq)