Riemann integration

[lowasser]

I know we haven't even merged derivatives yet, but I think this is actually well within our reach. The hardest part, I think, is simply showing that the equivalence of Fin mn and Fin m x Fin n has the expected relationship where (k, l) maps to nk + l, which is probably the key step in showing the limit converges.

From here, I think it's actually not a large step to Theorem 15 on the 100 Theorems, the Fundamental Theorem of Integral Calculus.

[lowasser]

That might actually be easier to prove by working directly with classical-Fin and constructing a new equivalence, rather than the preexisting product-Fin...