Changed to Lasse's suggestion.

coq/src/putnam_2009_b1.v

@@ -1,11 +1,9 @@
-Require Import List QArith Znumtheory Reals.
-Open Scope Q.
-Theorem putnam_2009_b1
-    (Factl := fix factl (l : list nat) : list nat :=
-        match l with
-        | nil => nil
-        | h :: t => fact h :: t
-    end)
-    : forall (q: Q), q > 0 -> exists (n d: list nat), (forall x, (In x n \/ In x d)-> prime (Z.of_nat x)) /\ 
-    inject_Z (Z.of_nat (fold_left Nat.mul (Factl n) 1%nat)) / inject_Z (Z.of_nat (fold_left Nat.mul (Factl d) 1%nat)) = q.
-Proof. Admitted.
+From mathcomp Require Import ssrbool seq ssrnat prime rat ssralg ssrnum ssrint.
+
+Local Open Scope ring_scope.
+
+Theorem putnam_2009_b1 :
+  let fact_prod (ls : seq nat) : rat := \prod_(i <- ls) (i`!)%:Q in
+  forall q : rat, q > 0 -> exists n d : seq nat,
+  all prime (n ++ d) /\ fact_prod n / fact_prod d = q.
+Proof. Admitted.