proposition: Lemma getAllBvectors_length_nz : forall n, length (getAllBvectors n) > 0.
proof: Proof. induction n; intuition; simpl in *. rewrite app_length. repeat rewrite map_length. apply Nat.lt_le_trans with (1 := IHn). now apply Nat.le_add_r. Qed.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith