Showing div is nonneg

Stream: new members

[Thomas Purdy]

Struggling with some metavariable stuff... want to prove that if 0 <= a and 0 <= b, where both a and b are integers, then 0 <= a/b. Using Int.div_nonneg gives me 0 <= Int.div a b, which I can't figure out how to cast to /, and just using normal div_nonneg fails

[Mario Carneiro]

You want docs#Int.ediv_nonneg

[Thomas Purdy]

Ah you're a lifesaver thank you

Mario Carneiro said:

You want docs#Int.ediv_nonneg