proposition: Fact mprod_factorial_Zp i n :〚mprod_an (i*p+1) n〛=〚fact n〛.
proof: Proof. rewrite mprod_factorial. induction n as [ | n IHn ]. + do 2 rewrite msum_0; auto. + do 2 (rewrite msum_plus1; auto). do 2 rewrite nat2Zp_mult; f_equal; auto. apply nat2Zp_inj. rewrite (Nat.add_comm n), <- Nat.add_assoc, Nat.add_comm. rewrite <- rem_plus_div; auto. * f_equal; lia. * apply divides_mult, divides_refl. Qed.
imports: Arith Nat Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums rel_iter) Undecidability.H10.ArithLibs(Zp)