proposition: Lemma shiftOut_to_list : forall n (v : Bvector n), shiftOut (VectorDef.to_list v) n = Some (v, nil).
proof: Proof. intuition. edestruct (shiftOut_Some (VectorDef.to_list v)). eapply le_refl_gen. symmetry. eapply (to_list_length v). destruct x. rewrite H. apply shiftOut_correct_inv in H. apply app_first_eq in H. intuition; subst. apply to_list_eq_inv in H0; subst. trivial. repeat rewrite to_list_length. trivial. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith Permutation