nat_div_mod_spec' x y : x - y * (x / y) = x mod y. Proof. apply nat_moveR_nV. rhs nrapply nat_add_comm. apply nat_div_mod_spec. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes