proposition: Fact Zp_mult_invert : forall x, is_gcd p (proj1_sig x) 1 -> { i | i ⊗ x = Op }.
proof: Proof. intros (x & Hx); simpl; intros H. destruct (bezout_generalized p x) as (u & v & g & l & H1 & H2 & H3 & _). generalize (is_gcd_fun H H2); intro; subst g. exists (exist _ (rem v p) (@div_rem_spec2 v p Hp)). apply Zp_inj; simpl. rewrite Nat.mul_comm, <- rem_scal. destruct H3 as (k & H3). rewrite Nat.mul_comm. rewrite <- rem_erase with (n := u) (1 := eq_refl). rewrite <- rem_erase with (n := k) (r := 1) (1 := eq_refl). f_equal. rewrite H1,H3; ring. 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)