n m : n * (m / n) <= m. Proof. set (tmp := n * (m / n)); rewrite (nat_div_mod_spec m n); unfold tmp; clear tmp. exact _. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes