proposition: Lemma iota_from_plus : forall k i j, iota_from i (k+j) = iota_from i k ++ iota_from (k+i) j.
proof: Proof. induction k; simpl. - trivial. - intros; rewrite IHk; repeat f_equal; abstract lia. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)