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