proposition: Lemma sorted_ge_trans n p l : n <= p -> sorted_ge p l -> sorted_ge n l.
proof: Proof. induction 2. - constructor 1. - constructor 2; eauto with arith. - constructor 3; [eauto with arith |assumption | assumption]. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)