proposition: Theorem alpha_nat_divides_2_pos m : alpha_nat b k * alpha_nat b k │ alpha_nat b m <-> k*alpha_nat b k │ m.
proof: Proof. Proof using Hak. destruct m as [ | m ]. + simpl; split; intros; apply divides_0. + destruct (divides_dec (S m) k) as [ (l & Hl) | C ]. * apply Zp_alpha_congruence_2 with (1 := Hl) (H2 := Hak2); try lia. apply alpha_square_nat; auto. intro; subst; discriminate. * split; intros H; exfalso; apply C. - rewrite <- alpha_nat_divisibility_1 with (1 := Hb). apply divides_trans with (2 := H), divides_mult, divides_refl. - apply divides_trans with (2 := H). rewrite Nat.mul_comm. apply divides_mult, divides_refl. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)