proposition: Lemma seq_cut n m: seq (n+m) = map lshift (seq n) ++ map rshift (seq m).
proof: Proof. induction n; simpl. rewrite <-(map_id (seq m)) at 1. apply map_ext. intros [i Hi]. apply eq_ord. reflexivity. rewrite IHn, map_app. f_equal. apply eq_ord. reflexivity. rewrite 3map_map. f_equal; apply map_ext; intros [i Hi]; apply eq_ord; reflexivity. Qed.
imports: List PeanoNat common comparisons