src/HOL/Fact.thy

     by (subst setprod_insert[symmetric]) (auto simp: atLeastAtMost_insertL)
   with assms show ?thesis
     by (induct r rule: nat.induct) (auto simp add: fact_div_fact Suc_diff_Suc mult_le_mono)
 qed
 
+lemma fact_numeral:  --{*Evaluation for specific numerals*}
+  "fact (numeral k) = (numeral k) * (fact (pred_numeral k))"
+  by (simp add: numeral_eq_Suc)
+
 end