proposition: Theorem RndPerm_In_support_length : forall n ls, In ls (getSupport (RndPerm n)) -> length ls = n.
proof: Proof. intuition. erewrite Permutation_length. 2:{ eapply Permutation_sym. eapply RndPerm_In_support. eauto. } eapply allNatsLt_length. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndListElem Permutation