proposition: Fact Z2Zp_inj u v :〘u〙=〘v〙<-> exists i, u-v = i*Z.of_nat p.
proof: Proof. split. + destruct (Z_pos_or_neg (u-v)) as [ H | H ]. * apply Z2Zp_inj_loc; lia. * intros H'; symmetry in H'. apply Z2Zp_inj_loc in H'; try lia. destruct H' as (i & Hi). exists (-i). apply f_equal with (f := Z.opp) in Hi. ring_simplify in Hi. rewrite <- Hi; ring. + intros (i & Hi). replace u with (v+(u-v)) by lia. rewrite Hi, Z2Zp_plus, Z2Zp_mult, Z2Zp_of_nat, nat2Zp_p; 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)