proposition: Lemma interval_not_empty : forall i j, i <= j -> interval i j <> nil.
proof: Proof. induction 1. - unfold interval. case_eq (S i - i). + intro; abstract lia. + simpl. destruct i; discriminate. - cbn. destruct i. cbn; discriminate. destruct i; cbn. discriminate. case_eq (m - i). intro; abstract lia. cbn; discriminate. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)