+lemma lt_n_plus_n_Sm : ∀n,m:nat.n < n + S m.
+intros; rewrite > sym_plus; apply (le_S_S n (m+n)); apply (le_plus_n m n); qed.
+
+lemma nth_concat_lt_len:
+ ∀T:Type.∀l1,l2:list T.∀def.∀i.i < len l1 → nth (l1@l2) def i = nth l1 def i.
+intros 4; elim l1; [cases (not_le_Sn_O ? H)] cases i in H H1; simplify; intros;
+[reflexivity| rewrite < H;[reflexivity] apply le_S_S_to_le; apply H1]
+qed.
+
+lemma nth_concat_ge_len:
+ ∀T:Type.∀l1,l2:list T.∀def.∀i.
+ len l1 ≤ i → nth (l1@l2) def i = nth l2 def (i - len l1).
+intros 4; elim l1; [ rewrite < minus_n_O; reflexivity]
+cases i in H1; simplify; intros; [cases (not_le_Sn_O ? H1)]
+apply H; apply le_S_S_to_le; apply H1;
+qed.
+
+lemma nth_len:
+ ∀T:Type.∀l1,l2:list T.∀def,x.
+ nth (l1@x::l2) def (len l1) = x.
+intros 2; elim l1;[reflexivity] simplify; apply H; qed.
+
+lemma all_bigger_can_concat_bigger:
+ ∀l1,l2,start,b,x,n.
+ (∀i.i< len l1 → nth_base l1 i < \fst b) →
+ (∀i.i< len l2 → \fst b ≤ nth_base l2 i) →
+ (∀i.i< len l1 → start ≤ i → x ≤ nth_base l1 i) →
+ start ≤ n → n < len (l1@b::l2) → x ≤ \fst b → x ≤ nth_base (l1@b::l2) n.
+intros; cases (cmp_nat n (len l1));
+[1: unfold nth_base; rewrite > (nth_concat_lt_len ????? H6);
+ apply (H2 n); assumption;
+|2: rewrite > H6; unfold nth_base; rewrite > nth_len; assumption;
+|3: unfold nth_base; rewrite > nth_concat_ge_len; [2: apply lt_to_le; assumption]
+ rewrite > len_concat in H4; simplify in H4; rewrite < plus_n_Sm in H4;
+ lapply linear le_S_S_to_le to H4 as K; rewrite > sym_plus in K;
+ lapply linear le_plus_to_minus to K as X;
+ generalize in match X; generalize in match (n - len l1); intro W; cases W; clear W X;
+ [intros; assumption] intros;
+ apply (q_le_trans ??? H5); apply (H1 n1); assumption;]
+qed.
+
+lemma sorted_head_smaller:
+ ∀l,p. sorted (p::l) → ∀i.i < len l → \fst p < nth_base l i.
+intro l; elim l; intros; [cases (not_le_Sn_O ? H1)] cases i in H2; simplify; intros;
+[1: inversion H1; [1,2: simplify; intros; destruct H3] intros; destruct H6; assumption;
+|2: apply (H p ? n ?); [apply (sorted_skip ??? H1)] apply le_S_S_to_le; apply H2]
+qed.
+
+
+alias symbol "pi1" = "pair pi1".
+alias symbol "lt" (instance 6) = "Q less than".
+alias symbol "lt" (instance 2) = "Q less than".
+alias symbol "and" = "logical and".
+lemma sorted_pivot:
+ ∀l1,l2,p. sorted (l1@p::l2) →
+ (∀i. i < len l1 → nth_base l1 i < \fst p) ∧
+ (∀i. i < len l2 → \fst p < nth_base l2 i).
+intro l; elim l;
+[1: split; [intros; cases (not_le_Sn_O ? H1);] intros;
+ apply sorted_head_smaller; assumption;
+|2: cases (H ?? (sorted_tail a (l1@p::l2) H1));
+ lapply depth = 0 (sorted_head_smaller (l1@p::l2) a H1) as Hs;
+ split; simplify; intros;
+ [1: cases i in H4; simplify; intros;
+ [1: lapply depth = 0 (Hs (len l1)) as HS;
+ unfold nth_base in HS; rewrite > nth_len in HS; apply HS;
+ rewrite > len_concat; simplify; apply lt_n_plus_n_Sm;
+ |2: apply (H2 n); apply le_S_S_to_le; apply H4]
+ |2: apply H3; assumption]]
+qed.
+
+definition eject_NxQ ≝