n m : n < m -> n / m = 0. Proof. intros H. snrapply (nat_div_unique _ _ _ _ H). by rewrite nat_mul_zero_r, nat_add_zero_l. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes