proposition: Lemma SubSeqAboveId : forall (un : SubSeq) (n : nat), le n (proj1_sig un n).
proof: Proof. intros [un inc]. induction n. simpl. apply Nat.le_0_l. simpl. simpl in IHn. specialize (inc n (S n)). unfold lt in inc. apply (Nat.le_trans _ (S (un n))). apply le_n_S. assumption. apply inc. apply Nat.le_refl. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits