n m (d : (n | m)) (gt0 : 0 < m) (gt1 : 1 < d.1) : n < m. Proof. rewrite <- d.2. snrapply (lt_leq_lt_trans (m:=1*n)). 1: rapply (leq_mul_l _ _ 0). srapply (nat_mul_r_strictly_monotone (l:=0)). rapply (gt_zero_divides n m). Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes