proposition: Lemma two_power_nat_equiv n : two_power_nat n = 2 ^ (Z.of_nat n).
proof: Proof. induction n as [|n IHn]. - trivial. - now rewrite Nat2Z.inj_succ, Z.pow_succ_r, <- IHn by apply Nat2Z.is_nonneg. Qed.
imports: Wf_nat ZArith_base Zcomplements Zpow_def