proposition: Lemma sorted_ge_Forall (n:nat) : forall l, sorted_ge n l -> Forall (fun x => n <= x) l.
proof: Proof. induction 1. - left. - now right. - right. + assumption. + eapply Forall_impl with (P := (fun x: nat => p <= x)); [|trivial]. intros; abstract lia. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)