proposition: Lemma shift_iota_from : forall i l, shift (iota_from i l) = iota_from (S 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)