proposition: Lemma Zp_alpha_congruence_2 : divides (ak*ak) am <-> divides (k*ak) m.
proof: Proof. Proof using l Hl Hk Hak H4 H3 H2 H1. rewrite Nat.mul_comm in H1. destruct H4 as (q & Hq1 & Hq2). split; intros H. + rewrite (proj1 (divides_nat2Zp _ _)) in Hq2; auto. symmetry in Hq2. rewrite <- Zp_mul_assoc in Hq2. apply Zp_invertible_eq_zero in Hq2; auto. rewrite <- nat2Zp_mult, <- divides_nat2Zp in Hq2. destruct Hq2 as (d & Hd); exists d; subst m. rewrite <- Nat.mul_cancel_r with (1 := Hak). rewrite <- Nat.mul_assoc, Hd; ring. + subst m. apply divides_mult_inv in H; auto. destruct H as (g & Hg); subst l. rewrite divides_nat2Zp with (Hp := H2). rewrite Hq2, nat2Zp_mult. do 2 rewrite <- Zp_mul_assoc. rewrite <- nat2Zp_mult, nat2Zp_p. do 2 rewrite (Zp_mul_comm _ _ (Zp_zero H2)), Zp_mult_zero. trivial. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)