How can we know what Dafny knows? i.e., is this specified somewhere? e.g., commented section below not known to Dafny.
Can I teach the commented theorem to Dafny, for example?
method WhatDafnyKnows(s: int, r: int, t: int)
//assert g != 0 && a % g == 0 && b % g == 0 ==> (a + b) % g == 0;
assert s * (t + r) == s * t + s * r;