proposition: Fact Zp_invertible_spec x : Zp_invertible x <-> is_gcd p (proj1_sig x) 1.
proof: Proof. split. + intros (i & Hi); revert Hi; apply Zp_mult_revert. + intros H; destruct (Zp_mult_invert _ H) as (i & ?); exists i; 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)