proposition: Fact nat2Zp_choose : forall x, x = Zp \/ x = Op \/ x = ∸ Op \/ exists m, (1 < m < p-1)%nat /\〚m〛= x.
proof: Proof. intros (x & Hx). destruct x as [ | [ | x ] ]. + left; apply Zp_inj; simpl; auto. + right; left; apply Zp_inj; simpl; rewrite rem_lt; auto. + destruct (eq_nat_dec (S (S x)) (p-1)) as [ H | H ]. * do 2 right; left. rewrite <- nat2Zp_minus_one. apply Zp_inj; simpl; rewrite rem_lt; lia. * do 3 right; exists (S (S x)); split; try lia. apply Zp_inj; simpl; rewrite rem_lt; lia. 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)