proposition: Lemma sorted_ge_not_In (n:nat) : forall l, sorted_ge (S n) l -> ~ In n l.
proof: Proof. intros l H; generalize (sorted_ge_Forall _ _ H); intros H0 H1. rewrite Forall_forall in H0. generalize (H0 n). intro H2; generalize (H2 H1). abstract lia. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)