prove mod-dist-+ using mod-uniq
open ≡-Reasoning locally
use DecTotalOrder module
add some lemmas
prove mod-uniq and div-uniq