proposition: Lemma rat_of_Z_pow z n : rat_of_Z (z ^ Z.of_nat n) = rat_of_Z z ^ n.
proof: Proof. rewrite /exprz -rmorphXn -Zpower_nat_Z; congr rat_of_Z. by elim: n => //= n ->; rewrite exprS. Qed.
imports: HB(structures) ZArith mathcomp(all_ssreflect all_algebra) tactics