proposition: Fact Z2Zp_zero_inv u : 〘u〙= Zp_zero -> exists v, (u = Z.of_nat p * v)%Z.
proof: Proof. intros H. rewrite <- Z2Zp_zero in H. apply Z2Zp_inj in H. destruct H as (y & Hy); exists y. rewrite Z.mul_comm, <- Hy; 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)