{n n' m m'} : n < m -> n' < m' -> n * n' < m * m'. Proof. intros H1 H2. nrapply (lt_leq_lt_trans (m:=n * m')). 1: rapply nat_mul_l_monotone. rapply nat_mul_r_strictly_monotone. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids