proposition: Fact Zp_invert_not_fix n : (1 < n < p-1)%nat -> inv〚n〛<>〚n〛.
proof: Proof. intros H1 H2. apply Zp_invert_fix in H2. destruct H2 as [ H2 | [ H2 | H2 ] ]. + rewrite <- nat2Zp_zero in H2. apply nat2Zp_inj in H2. rewrite rem_lt, rem_lt in H2; lia. + rewrite <- nat2Zp_one in H2. apply nat2Zp_inj in H2. rewrite rem_lt, rem_lt in H2; lia. + rewrite <- nat2Zp_minus_one in H2. apply nat2Zp_inj in H2. rewrite rem_lt, rem_lt in H2; 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)