fact: Fixpoint Interval_list i : nat * nat := match i with | 0 => (0, F 0) | S i' => let x := snd (Interval_list i') in (x, x + F i) end.
imports: Coq(Morphisms Euclid Peano Lia) Coq(Compare) CoLoR(LogicUtil EqUtil BoolUtil NatCompat RelUtil)