fact: Fixpoint iterateN2Func (n i j : nat) (f : nat -> nat -> prod nat nat) := match n with | O => pair i j | S p => let (k,l) := iterateN2Func p i j f in f k l end.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits