proposition: Theorem Wilson_theorem p : 2 <= p -> prime p <-> divides p (fact (p-1)+1).
proof: Proof. intros H1; split. + intros H2. assert (Hp : p <> 0) by lia. rewrite divides_nat2Zp with (Hp := Hp). rewrite nat2Zp_plus, Wilson_thm_1; auto. rewrite nat2Zp_one, Zp_add_comm, Zp_minus; auto. + intros H2; split; try lia. intros q Hq. destruct (eq_nat_dec q p) as [ Hp | Hp ]; auto. generalize (divides_trans Hq H2); intros H3. apply divides_plus_inv in H3. - apply divides_1_inv in H3; auto. - apply divides_fact_lt. apply divides_not_0_interval in Hq; 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)