proposition: Lemma iota_from_app n p : iota_from n (S p) = iota_from n p ++ (n+p::nil)%nat.
proof: Proof. revert n; induction p; simpl. - intros; f_equal; abstract lia. - intros; f_equal; replace (n + S p)%nat with (S n + p)%nat. + rewrite <- IHp; auto. + abstract lia. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)