proposition: Lemma in_getSupport_RndNat : forall x k, x < k -> In x (getSupport (RndNat k)).
proof: Proof. intuition. simpl. eapply filter_In. split. eapply in_getUnique. eapply in_flatten. econstructor. split. eapply in_map_iff. econstructor. split. eapply eq_refl. eapply in_getAllBvectors. simpl. left. eapply bvToNat_natToBv_inverse. eapply lognat_monotonic. trivial. unfold ltNatBool. destruct (lt_dec x k); intuition. Qed.
imports: FCF.Crypto Permutation FCF.NotationV1