one key grid theorem.json

{
  "assume": "s=h*m with integer m; gcd(p,q)=1",
  "reduce": "(p/q)*s in hZ iff p*m/q is integer",
  "necessity": "q divides p*m; coprimality implies q divides m",
  "sufficiency": "m=q*t gives output h*p*t",
  "domain": "h*q*Z"
}