Definition natlehandmultrinv (n m k : nat) : k ≠ 0 -> n * k ≤ m * k -> n ≤ m. Proof. intros r s. apply negnatgthtoleh; intro t. apply (natlehtonegnatgth _ _ s). apply (natgthandmultr _ _ _ r). assumption. Defined.