fact: Definition SubSeq : Type := { sub : nat -> nat | forall n p:nat, lt n p -> lt (sub n) (sub p) }.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits