{n m l} k : l < k -> n < m -> k * n < k * m. Proof. destruct k. 1: intro; contradiction (not_lt_zero_r _ H). intros _ H; induction k as [|k IHk] in |- *; exact _. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids