proposition: Fact mprod_factorial_mult n : fact (n*p) = expo n p * fact n * Ψ n.
proof: Proof. Proof using Hp. induction n as [ | n IHn ]. + rewrite Nat.mul_0_l, msum_0, mscal_0, fact_0; auto. + replace (S n*p) with (n*p+p) by ring. rewrite mprod_factorial, msum_plus, <- mprod_factorial; auto. replace p with (S (p-1)) at 2 by lia. rewrite msum_plus1; auto. rewrite <- Nat.add_assoc. replace (p-1+1) with p by lia. replace (n*p+p) with ((S n)*p) by ring. rewrite mscal_S, fact_S, msum_S. rewrite IHn. repeat rewrite Nat.mul_assoc. rewrite (Nat.mul_comm _ p). repeat rewrite <- Nat.mul_assoc. do 2 f_equal. rewrite (Nat.mul_comm (S n)). repeat rewrite <- Nat.mul_assoc; f_equal. repeat rewrite Nat.mul_assoc; f_equal. rewrite msum_ext with (f := fun i => n*p+i+1) (g := fun i => i+(n*p+1)). 2: intros; ring. rewrite <- msum_plus1; auto. Qed.
imports: Arith Nat Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums rel_iter) Undecidability.H10.ArithLibs(Zp)