#292 (Jul 9, 2016, 1:38:11 PM)

1. more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
   * * *
   more rules for setsum, setprod on intervals (detail / hgweb)
2. avoid to hide equality behind (output) abbreviation (detail / hgweb)
3. default rule for single-step reasoning (detail / hgweb)

Started by an SCM change