proposition: Theorem shiftOut_None_inv : forall n ls, shiftOut ls n = None -> n > length ls.
proof: Proof. induction n; destruct ls; intuition; simpl in *; try discriminate. apply ->Nat.succ_lt_mono. eapply IHn. case_eq (shiftOut ls n); intuition; trivial. rewrite H0 in H. destruct p. discriminate. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith