proposition: Theorem shiftOut_oneList : forall (n : nat), shiftOut (oneList n) n = Some (oneVector n, nil).
proof: Proof. induction n; intuition; simpl in *. rewrite IHn. trivial. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith