Mar 11, 2014 at 4:01 PM
Edited Mar 11, 2014 at 4:02 PM

Hi,
I'm surprised with the difficulties I find for proving any property involving the module operation %. The following is a basic property that I cannot prove
lemma test(a: int, b: int)
requires a > 0 && b >= 0;
ensures (a * b) % a == 0;
{
}
Does someone know how can I help Dafny to prove it?

