proposition: Lemma two_p_correct x : two_p x = 2^x.
proof: Proof. Proof (two_p_equiv x). Theorem two_p_is_exp x y : 0 <= x -> 0 <= y -> two_p (x + y) = two_p x * two_p y. Proof. rewrite !two_p_equiv. apply Z.pow_add_r. Qed.
imports: Wf_nat ZArith_base Zcomplements Zpow_def