proposition: Fact Zp_invert_stable n : (1 < n < p-1)%nat -> exists m, (1 < m < p-1)%nat /\〚m〛= inv〚n〛.
proof: Proof. intros Hn. destruct (nat2Zp_choose (inv 〚n〛)) as [ H | [ H | [ H | H ] ] ]; auto; exfalso; apply f_equal with (f := inv) in H; rewrite Zp_invert_involutive in H; symmetry in H. + rewrite Zp_invert_spec1 in H. rewrite <- nat2Zp_zero, nat2Zp_inj in H. rewrite rem_lt, rem_lt in H; lia. + rewrite Zp_invert_one, <- nat2Zp_one in H. rewrite nat2Zp_inj, rem_lt, rem_lt in H; lia. + rewrite Zp_invert_minus_one, <- nat2Zp_minus_one in H. rewrite nat2Zp_inj, rem_lt, rem_lt in H; 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)