proposition: Lemma RndNat_unchecked_lt_support : forall n v, v < n -> In v (getSupport (RndNat_unchecked n)).
proof: Proof. intuition. unfold RndNat_unchecked. eapply getSupport_In_Seq. eapply in_getAllBvectors. simpl. left. eapply bvToNat_natToBv_inverse. eapply lognat_monotonic. lia. Qed.
imports: FCF.Crypto Permutation FCF.NotationV1