proposition: Theorem birthday_paradox_min : let l := picks 22 (enumerate 365) in 2 * length (filter collision l) < length l.
proof: Proof. intros l; unfold l. apply Nat2Z.inj_lt. rewrite Nat2Z.inj_mul. repeat rewrite <-Zlength_correct. rewrite Zlength_filter. rewrite length_no_collision_picks. 2:apply enumerate_no_collisions. repeat rewrite Zlength_picks. reflexivity. Qed.
imports: Arith ZArith List Lia