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