proposition: Lemma SubSeqInvFound : forall (un : SubSeq) (n k : nat), (SubSeqInv un n k <= n <-> proj1_sig un (SubSeqInv un n k) = n)%nat.
proof: Proof. intros. generalize dependent n. induction k. - simpl. split. + intro. destruct (Nat.eq_dec (proj1_sig un O) n). assumption. exfalso. apply (Nat.lt_nge n (S n)). apply Nat.le_refl. assumption. + intro. destruct (Nat.eq_dec (proj1_sig un O) n). apply Nat.le_0_l. exfalso. pose proof (SubSeqAboveId un n). destruct un. simpl in H. simpl in n0. simpl in H0. apply (Nat.lt_nge (x n) (x (S n))). apply l. apply Nat.le_refl. rewrite H. assumption. - split. + intro. simpl. simpl in H. destruct (Nat.eq_dec (proj1_sig un (S k)) n). assumption. apply IHk. assumption. + simpl. intro. destruct (Nat.eq_dec (proj1_sig un (S k)) n). rewrite <- e. apply SubSeqAboveId. apply IHk. assumption. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits