proposition: Lemma shiftOut_skipn : forall n (v : Bvector n) s s', shiftOut s n = Some (v, s') -> s' = skipn n s.
proof: Proof. induction n; intuition; simpl in *. rewrite shiftOut_0 in H. inversion H; clear H; subst. trivial. destruct s; simpl in *. discriminate. case_eq (shiftOut s n); intuition; rewrite H0 in H. destruct p. inversion H; clear H; subst. eauto. discriminate. Qed.
imports: FCF.Comp FCF.Blist FCF.Fold Permutation micromega.Lia