improve reduction

Author: thery

factorion.v

@@ -268,7 +268,14 @@ case=> [d9E|].
     rewrite nE mE1 divnMDl ?expn_gt0 //.
     rewrite mE divn_small; last by rewrite ltn_mod expn_gt0.
     by rewrite addn0 mulnC.
-  by rewrite nE sum_factMD // -p1E N2Nat.inj_add.
+  rewrite nE sum_factMD // -p1E N2Nat.inj_add.
+  have -> : N.to_nat (362880) = N.to_nat (9 * (8 * (7 * (720)))).
+    by congr N.to_nat.
+  rewrite [N.to_nat (9 * _)]N2Nat.inj_mul.
+  rewrite [N.to_nat (8 * _)]N2Nat.inj_mul.
+  rewrite [N.to_nat (7 * _)]N2Nat.inj_mul.
+  rewrite 3!factS.
+  by congr ((_ * (_ * (_ * _)%coq_nat)%coq_nat)%coq_nat + _)%coq_nat.
 move=> d d1E.
 suff : d1 < 10 by rewrite d1E.
 by apply: ltn_pdigit.