Add lemma Power_pos for power in stdlib
From SPARK, users have apparently seen some improvements adding the following lemma to the Power theory.
lemma Power_pos:
forall x y. x > 0 /\ y >= 0 -> power x y > 0
This really looks like Power_non_neg
but adding this version apparently helps them more.
This issue to ask if you think it would be ok for me to add it in Why3 (would it be useful for Why3 users ?).