proposition: Theorem Wilson_thm_1 :〚fact (p-1)〛= ∸Op.
proof: Proof. Proof using Hp'. replace (p-1)%nat with (S (p-2))%nat by lia. rewrite Zp_lprod_fact. destruct (eq_nat_dec p 2) as [ H1 | H1 ]. + rewrite H1; simpl map; rewrite Zp_lprod_nil. rewrite <- nat2Zp_minus_one; apply nat2Zp_inj. rewrite H1; auto. + replace (p-2)%nat with (p-3+1)%nat by lia. rewrite list_an_plus, map_app, Zp_lprod_app. replace (p-3+2)%nat with (p-1)%nat by lia. simpl list_an at 2; unfold map at 2. rewrite Zp_lprod_cons, Zp_lprod_nil. rewrite Zp_mult_autoinv. * rewrite nat2Zp_minus_one; ring. * intros H. apply list_has_dup_map_inv in H. - revert H; apply not_list_an_has_dup. - intros x y; do 2 rewrite list_an_spec. intros Hx Hy. rewrite nat2Zp_inj, rem_lt, rem_lt; auto; lia. * intros x; rewrite in_map_iff. intros (n & ? & Hn); subst. rewrite list_an_spec in Hn. split; [ | split ]. - intros H. rewrite <- nat2Zp_zero in H. apply nat2Zp_inj in H. rewrite rem_of_0, rem_lt in H; lia. - apply Zp_invert_not_fix; lia. - destruct Zp_invert_stable with n as (m & G1 & G2); try lia. apply in_map_iff. exists m; split; auto. apply list_an_spec; 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)