proposition: Lemma inj_pow (x y : nat) : Z.of_nat (x ^ y) = (Z.of_nat x) ^ (Z.of_nat y).
proof: Proof. induction y as [|y IH]; [by rewrite Z.pow_0_r, Nat.pow_0_r|]. by rewrite Nat.pow_succ_r, Nat2Z.inj_succ, Z.pow_succ_r, Nat2Z.inj_mul, IH by auto with zpos. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)