module operation

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?