proposition: Fact Zp_invert_eq_not_zero x y : x <> Zp -> inv x = y <-> y ⊗ x = Op.
proof: Proof. intros H1. split. + intros H2; rewrite <- H2; apply Zp_invert_spec2; auto. + intros H2. apply Zp_invert_spec2 in H1. rewrite <- (Zp_mult_one (inv x)) , <- H2, <- Zp_mul_assoc, (Zp_mul_comm x), H1, Zp_mul_comm, Zp_mult_one. trivial. 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)