proposition: Lemma RndNat_support_lt : forall n x, In x (getSupport (RndNat n)) -> x < n.
proof: Proof. intuition. unfold RndNat in *. simpl in *. eapply filter_In in H. intuition. unfold ltNatBool in *. destruct (lt_dec x n); congruence. Qed.
imports: FCF.Crypto Permutation FCF.NotationV1