proposition: Lemma Zdivide_square_rev : forall a b, (a * a | b * b) -> (a | b).
proof: Proof. intros a b D. destruct (Z.eq_dec a 0). subst; simpl in D. destruct D as (q, Hq); ring_simplify (q * 0) in Hq. destruct b; inversion Hq. exists 0; ring. exists (b / a). rewrite Zmult_comm, Z_mult_div_mod; auto. Abort. Lemma Zpow_mod (a b m : Z) : (a ^ b) mod m = ((a mod m) ^ b) mod m. Proof. assert (b < 0 \/ 0 <= b) as [bz | bz] by lia. - rewrite 2 Z.pow_neg_r; auto. - rewrite <-(Z2Nat.id b); auto. rewrite <-2Zpower_nat_Z. generalize (Z.to_nat b); intros n. clear b bz. destruct (Z.eq_dec m 0). + subst. now rewrite !Zmod_0_r. + induction n. easy. simpl. rewrite Z.mul_mod, IHn, Z.mul_mod_idemp_r; auto. Qed.
imports: ZArith Lia Znumtheory