add quotient cancelling and nat_mul divisibility monotonicty

[Alizter]

In this PR we add a lemma showing that multiplication is monotone with respect to divisibility as an order.

We also give two lemmas allow us to cancel common factors in quotients, given suitable conditions.

[jdchristensen]

This is also true when m = 0, easily. In fact, it is also true without the hypothesis that (m | n). Here's a proof that uses nat_zero_or_gt_zero from #2062.

Definition nat_div_cancel_mul_l n m k
  : 0 < k -> (k * n) / (k * m) = n / m.
Proof.
  intro kp.
  destruct (nat_zero_or_gt_zero m) as [[] | mp].
  1: by rewrite nat_mul_zero_r.
  symmetry; nrapply (nat_div_unique _ _ _ (k * (n mod m))).
  1: rapply nat_mul_l_strictly_monotone.
  rewrite <- nat_mul_assoc.
  rewrite <- nat_dist_l.
  apply ap.
  symmetry; apply nat_div_mod_spec.
Defined.

While I'm at it, here's a similar fact about mod:

Definition nat_mod_mul_l n m k
  : (k * n) mod (k * m) = k * (n mod m).
Proof.
  destruct (nat_zero_or_gt_zero k) as [[] | kp].
  1: reflexivity.
  destruct (nat_zero_or_gt_zero m) as [[] | mp].
  1: by rewrite nat_mul_zero_r.
  symmetry; apply (nat_mod_unique _ _ (n / m)).
  1: rapply nat_mul_l_strictly_monotone.
  rewrite <- nat_mul_assoc.
  rewrite <- nat_dist_l.
  apply ap.
  symmetry; apply nat_div_mod_spec.
Defined.

Maybe the two proofs can even be combined, using nat_div_mod_spec?

[Alizter]

That's a good point. I'll wait until #2062 is merged and have a go at combining these two facts.

[Alizter]

I didn't see a way to combine both lemmas in the end, partly because the assumptions on k are different.

[jdchristensen]

Ok, this LGTM!