proposition: Fact nat2Zp_invertible_prime n : (0 < n < p)%nat -> Zp_invertible 〚n〛.
proof: Proof. Proof using Hp'. intros Hn. apply Zp_invertible_prime; auto. intros H. apply divides_nat2Zp in H. destruct H as ([ | k ] & Hk). + simpl in Hk; lia. + revert Hn; rewrite Hk; simpl. generalize (k*p)%nat; intros; 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)