Definition natlehandmultl (n m k : nat) : n ≤ m -> k * n ≤ k * m. Proof. intros r. apply negnatgthtoleh; intro t. apply (natlehtonegnatgth _ _ r). apply (natgthandmultlinv _ _ k). assumption. Defined.