proposition: Lemma iota_from_sorted_ge : forall p n q : nat, (q <= n)%nat -> sorted_ge q (iota_from n p).
proof: Proof. induction p. - constructor. - simpl; destruct p. + constructor 2 ; auto. + simpl; simpl in IHp; constructor 3; auto. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)