proposition: Fact Zp_invertible_prime x : prime p -> Zp_invertible x <-> x <> Zp.
proof: Proof. intros H. split. + intros (i & Hi) E. subst. rewrite Zp_mul_comm, Zp_mult_zero, Zp_zero_is_one in Hi. apply prime_ge_2 in H; lia. + intros Hx. destruct (nat2Zp_surj x) as (u & _ & Hu). rewrite Hu; apply nat2Zp_invertible. destruct (prime_gcd u H) as [ H1 | H1 ]; auto. destruct Hx. rewrite Hu; apply divides_nat2Zp; auto. 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)