even powers

Stream: Is there code for X?

[Benjamin Davidson]

Is there a lemma that states that any real number raised to an even natural power is nonnegative?

[Johan Commelin]

I don't think so. The proof should be a 1-liner (maybe 2), but the lemma itself isn't there yet I think

[Benjamin Davidson]

Would that be via pow_bit0_nonneg? That's the only thing I came across that seems to relate to this.

[Johan Commelin]

ooh, that might do it.

[Johan Commelin]

I would have extracted n = 2 * k, and then rewrite to (x ^ k) ^ 2 and use pow_two_nonneg

[Johan Commelin]

but your version might be a step shorter

[Benjamin Davidson]

Oh that's clever as well! I'll try with pow_bit0_nonneg since the more I look at it the simpler it seems, but either way should be pretty easy. Cheers!