proposition: Theorem shiftOut_correct_inv : forall n ls ls' v, shiftOut ls n = Some (v, ls') -> ls = (Vector.to_list v) ++ ls'.
proof: Proof. induction n; destruct ls; intuition; simpl in *. inversion H; clear H; subst. simpl. trivial. inversion H; clear H; subst. simpl. trivial. discriminate. case_eq (shiftOut ls n); intuition. rewrite H0 in H. destruct p. inversion H; clear H; subst. simpl. f_equal. apply IHn in H0. subst. trivial. rewrite H0 in H. discriminate. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith