proposition: Fact Zp_prime_invert : prime p -> forall x, x <> Zp -> { i | i ⊗ x = Op }.
proof: Proof. intros Hp' x Hx. apply Zp_mult_invert. destruct x; simpl in *. destruct (prime_gcd x Hp') as [ | H ]; auto. exfalso; apply Hx, Zp_inj; simpl. destruct H as ([ | k ] & Hk); simpl in Hk; auto. revert Hk; generalize (k* p); 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)