proposition: Lemma but_last_interval i j: i < j -> but_last i (interval (S i) (S j)) = i:: interval (S i) j.
proof: Proof. intros. unfold interval. specialize (but_last_iota_from (S j - S i) i). intro. replace (S (S j) - S i) with (S (S j - S i)). replace (S j) with (i + S (S j - S i)) at 3. 2: lia. 2:lia. auto. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)