proposition: Lemma sqrt_bpow : forall e, sqrt (bpow (2 * e)) = bpow e.
proof: Proof. intro e. change 2%Z with (1 + 1)%Z; rewrite Z.mul_add_distr_r, Z.mul_1_l, bpow_plus. apply sqrt_square, bpow_ge_0. Qed.
imports: Coq(Psatz Reals ZArith) Zaux