n k : k < n -> k mod n = k. Proof. intros H. lhs_V nrapply nat_div_mod_spec'. rewrite nat_div_lt. - rewrite nat_mul_zero_r. apply nat_sub_zero_r. - exact H. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes