Lemma natdivremandmultr (n m k : nat) (ism : m ≠ 0) (ismk : (m * k) ≠ 0) : dirprod (paths (natdiv (n * k) (m * k)) (natdiv n m)) (paths (natrem (n * k) (m * k)) ((natrem n m) * k)). Proof. intros. rewrite (natmultcomm m k). rewrite (natmultcomm m k) in ismk. rewrite (natmultcomm n k). rewrite (natmultcomm (natrem _ _) k). apply (natdivremandmultl _ _ _ ism ismk). Defined.