fact: Fixpoint SubSeqInv (un : SubSeq) (n p : nat) : nat := if Nat.eq_dec (proj1_sig un p) n then p else match p with | O => S n | S k => SubSeqInv un n k end.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits