proposition: Lemma shiftOut_lt : forall ls n, length ls < n -> shiftOut ls n = None.
proof: Proof. induction ls; intuition; simpl in *. destruct n. lia. trivial. destruct n. lia. rewrite IHls. trivial. lia. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith