proposition: Fact Zp_invertible_factorial n : (n < p)%nat -> Zp_invertible 〚fact n〛.
proof: Proof. Proof using Hp'. induction n as [ | n IHn ]; intros Hn. + rewrite fact_0; apply nat2Zp_invertible_prime; lia. + rewrite fact_S, nat2Zp_mult; apply Zp_mult_invertible. * apply nat2Zp_invertible_prime; lia. * apply IHn; 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)