proposition: Lemma ShouldReplaceSubSeq : forall (sub : SubSeq) (n : nat), le n (proj1_sig sub n).
proof: Proof. induction n. - apply Nat.le_0_l. - destruct sub; simpl. simpl in IHn. specialize (l n (S n) (Nat.le_refl _)). apply (Nat.le_trans _ (S (x n))). apply le_n_S, IHn. exact l. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal