Definition natgthandmultlinv (n m k : nat) : (k * n) > (k * m) -> n > m. Proof. revert m k. induction n as [ | n IHn ]. - intros m k g. rewrite (natmultn0 k) in g. induction (negnatgth0n _ g). - intro m. destruct m as [ | m ]. + intros. apply (natgthsn0 _). + intros k g. rewrite (multnsm k n) in g. rewrite (multnsm k m) in g. apply (IHn m k (natgthandpluslinv _ _ k g)). Defined.