proposition: Lemma mprod_factorial_euclid n r : fact (n*p+r) = expo n p * fact n * φ n r * Ψ n.
proof: Proof. Proof using Hp. rewrite mprod_factorial, msum_plus; auto. rewrite <- mprod_factorial. rewrite msum_ext with (f := fun i => n*p+i+1) (g := fun i => i+(n*p+1)). 2: intros; ring. rewrite mprod_factorial_mult; auto; ring. Qed.
imports: Arith Nat Lia List Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums rel_iter) Undecidability.H10.ArithLibs(Zp)