proposition: Lemma rndNat_sumList : forall (A : Set)(f : nat -> Comp A) n (nzn : nz n) x, evalDist (i <-$ RndNat n; f i) x == sumList (forNats n) (fun i => (1 / n) * (evalDist (f i) x)).
proof: Proof. intuition. unfold evalDist. fold evalDist. rewrite sumList_permutation. 2:{ eapply (@NoDup_Permutation _ _ (forNats n)). eapply getSupport_NoDup. eapply forNats_NoDup. intuition. eapply forNats_In. eapply RndNat_support_lt. trivial. eapply in_getSupport_RndNat. eapply forNats_In. trivial. } eapply sumList_body_eq. intuition. eapply ratMult_eqRat_compat; intuition. eapply RndNat_prob. eapply forNats_In. trivial. Qed.
imports: FCF.Crypto Permutation FCF.NotationV1