Can't solve Assignment09_05: don't know how to use hoare_if...

[ik1ne]

I managed to solve 09_05, but I didn't used hoare_if(with definition of 09_00). And I think it is the worst way to prove 09_05. In fact, I don't know how to use Theorem hoare_if in assignment file. Can you give me a hint, or an example by proving Example if_example in Hoare.v? (using hoare_if from Assignment09_00.v, since there is already a proof using Theorem hoare_if from Hoare.v)

[jaewooklee93]

123 #124

[ik1ne]

@jaewooklee93 Thank you! I've read #123, but haven't read #124 since it was closed before I check it, so I thought nobody was asking for it.