proposition: Lemma sorted_ge_iff : forall l n, sorted_ge n l <-> Sorted lt l /\ List.Forall (fun i => n <= i) l.
proof: Proof. intros. rewrite Sorted_LocallySorted_iff. apply sorted_ge_iff0. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)