proposition: Lemma SubSeqInvNotFound : forall (un : SubSeq) (n k : nat), SubSeqInv un n k = S n <-> (forall p:nat, le p k -> proj1_sig un p <> n).
proof: Proof. intros. generalize dependent n. induction k. - split. + intros. intro absurd. simpl in H. destruct (Nat.eq_dec (proj1_sig un O) n). discriminate. destruct un. simpl in absurd. simpl in n0. inversion H0. subst p. contradiction. + intros. simpl. destruct (Nat.eq_dec (proj1_sig un O) n). exfalso. exact (H O (Nat.le_refl 0) e). reflexivity. - split. + intros. intro absurd. simpl in H. destruct (Nat.eq_dec (proj1_sig un (S k)) n). inversion H. subst k. pose proof (SubSeqAboveId un (S n)). rewrite e in H1. apply (Nat.lt_nge n (S n)). apply Nat.le_refl. assumption. apply Nat.le_succ_r in H0. destruct H0. specialize (IHk n) as [IHk _]. specialize (IHk H p H0). contradiction. subst p. contradiction. + intros. simpl. destruct (Nat.eq_dec (proj1_sig un (S k)) n). exfalso. specialize (H (S k) (Nat.le_refl _)). contradiction. apply IHk. intros. apply H. apply (Nat.le_trans _ k). assumption. apply le_S. apply Nat.le_refl. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits