proposition: Theorem shiftOut_Some_inv : forall n ls v ls', shiftOut ls n = Some (v, ls') -> (n <= length ls)%nat.
proof: Proof. induction n; destruct ls; intuition; simpl in *; try discriminate. apply le_n_S. case_eq (shiftOut ls n); intuition. destruct p. eauto. rewrite H0 in H. discriminate. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith