proposition: Lemma sqrt_bpow_ge : forall e, (bpow (e / 2) <= sqrt (bpow e))%R.
proof: Proof. intro e. rewrite <- (sqrt_square (bpow _)); [|now apply bpow_ge_0]. apply sqrt_le_1_alt; rewrite <- bpow_plus; apply bpow_le. now replace (_ + _)%Z with (2 * (e / 2))%Z by ring; apply Z_mult_div_ge. Qed.
imports: Coq(Psatz Reals ZArith) Zaux