Lemma natdivremandmultl (n m k : nat) (ism : m ≠ 0) (iskm : (k * m) ≠ 0) : dirprod (paths (natdiv (k * n) (k * m)) (natdiv n m)) (paths (natrem (k * n) (k * m)) (k * (natrem n m))). Proof. intros. set (ak := natdiv (k * n) (k * m)). set (bk := natrem (k * n) (k * m)). set (a := natdiv n m). set (b := natrem n m). assert (e1 : paths (bk + ak * (k * m)) ((b * k) + a * (k * m))). { unfold ak. unfold bk. rewrite (pathsinv0 (natdivremrule (k * n) (k * m) iskm)). rewrite (natmultcomm k m). rewrite (pathsinv0 (natmultassoc _ _ _)). rewrite (pathsinv0 (natrdistr _ _ _)). unfold a. unfold b. rewrite (pathsinv0 (natdivremrule n m ism)). apply (natmultcomm k n). } set (l1 := lthnatrem n m ism). set (l1' := (natlthandmultr _ _ _ (natneq0andmultlinv _ _ iskm) l1)). rewrite (natmultcomm m k) in l1'. set (int := natdivremunique _ _ _ _ _ (lthnatrem (k * n) (k * m) iskm) l1' e1). split with (pr1 int). rewrite (natmultcomm k b). apply (pr2 int). Defined.