fact: Definition diagSeq {X : Type} (u : nat -> nat -> X) (p : nat) := let (n, k) := diagPlaneInv p in u n k.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits