proposition: Lemma RndNat_support_length : forall n, length (getSupport (RndNat n)) = n.
proof: Proof. intuition. rewrite (@Permutation_length _ _ (forNats n)). eapply forNats_length. eapply NoDup_Permutation. eapply getSupport_NoDup. eapply forNats_NoDup. intuition. eapply forNats_In. eapply RndNat_support_lt; intuition. eapply in_getSupport_RndNat. eapply forNats_In; intuition. Qed.
imports: FCF.Crypto Permutation FCF.NotationV1