fact: Definition diagPlaneInvNext i j : prod nat nat := match i with | O => pair (S j) O | S k => pair k (S j) end.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits