fact: Definition diagPlaneInv (n : nat) : prod nat nat := iterateN2Func n O O diagPlaneInvNext.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits