Definition natgthandmultl (n m k : nat) : k ≠ 0 -> n > m -> (k * n) > (k * m). Proof. revert m k. induction n as [ | n IHn ]. - intros m k g g'. induction (negnatgth0n _ g'). - intro m. destruct m as [ | m ]. + intros k g g'. rewrite (natmultn0 k). rewrite (multnsm k n). apply (natgehgthtrans _ _ _ (natgehplusnmn k (k* n)) (natneq0togth0 _ g)). + intros k g g'. rewrite (multnsm k n). rewrite (multnsm k m). apply (natgthandplusl _ _ _). apply (IHn m k g g'). Defined.