proposition: Fact Zp_zero_is_one : Zp = Op <-> p = 1.
proof: Proof. split. + intros H; apply f_equal with (f := @proj1_sig _ _) in H; simpl in H. symmetry in H. apply divides_rem_eq, divides_1_inv in H; auto. + intros; apply Zp_inj; simpl; subst; rewrite rem_diag; 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)