proposition: Lemma unshift_iota_from : forall i l, unshift (iota_from (S i) l) = iota_from i l.
proof: Proof. intros i l; revert i;induction l. - trivial. - cbn. intro; now rewrite IHl. Qed.
imports: Coq(Sorting.Sorted Compare_dec Sorting.Sorted)