src/HOL/Binomial.thy

                  (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1) =
              of_nat (2 ^ (2 * (Suc n))) * pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n)"
     by (simp add: of_nat_mult field_simps pochhammer_rec')
   finally show ?case .
 qed simp
+
+lemma fact_double:
+  "fact (2 * n) = (2 ^ (2 * n) * pochhammer (1 / 2) n * fact n :: 'a :: field_char_0)"
+  using pochhammer_double[of "1/2::'a" n] by (simp add: pochhammer_fact)
 
 lemma pochhammer_absorb_comp:
   "((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k"
   (is "?lhs = ?rhs")
 proof -