x y q r (H : r < y) (p : y * q + r = x) : x mod y = r := snd (nat_div_mod_unique y (x / y) q (x mod y) r _ _ (p @ nat_div_mod_spec x y)^).
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes