proposition: Lemma SubSeqInvInit : forall (un : SubSeq) (n : nat), SubSeqInv un (proj1_sig un O) n = O.
proof: Proof. induction n. - simpl. destruct (Nat.eq_dec (proj1_sig un O) (proj1_sig un O)). reflexivity. exfalso. exact (n (eq_refl _)). - simpl. destruct (Nat.eq_dec (proj1_sig un (S n)) (proj1_sig un O)). exfalso. destruct un. simpl in e. apply (Nat.lt_nge (x O) (x (S n))). apply l. apply le_n_S. apply Nat.le_0_l. rewrite e. apply Nat.le_refl. apply IHn. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits