Use a smart constructor to build dfrac

Addresses part of #354.

I didn't make an attempt to hide the old API. We could do that by wrapping the inductive in a module and locally importing it.