proposition: Fact mprod_factorial n : fact n = mprod_an 1 n.
proof: Proof. induction n as [ | n IHn ]. + rewrite msum_0; auto. + rewrite msum_plus1; auto. rewrite Nat.mul_comm, <- IHn, fact_S. f_equal; lia. Qed.
imports: Arith Nat Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums rel_iter) Undecidability.H10.ArithLibs(Zp)