proposition: Fact Zp_lprod_fact n : 〚fact (S n)〛= Zp_lprod (map nat2Zp (list_an 2 n)).
proof: Proof. Proof using Hp'. induction n as [ | n IHn ]. + apply Zp_inj; simpl; auto. + rewrite fact_S, nat2Zp_mult. replace (S n)%nat with (n+1)%nat by lia. rewrite list_an_plus, map_app, Zp_lprod_app, <- IHn, Zp_mul_comm. f_equal. * do 2 f_equal; lia. * simpl list_an; unfold map. rewrite Zp_lprod_cons, Zp_mul_comm, Zp_mult_one. f_equal; lia. Qed.
imports: Arith Lia ZArith List Permutation Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list gcd prime binomial sums php) Undecidability.H10.ArithLibs(matrix)