x y : x = y * (x / y) + x mod y. Proof. destruct y as [|y]; only 1: reflexivity. pose proof (p := fst (nat_div_mod_helper_spec x y 0 y _)). by rewrite nat_mul_zero_r, nat_sub_cancel, 2 nat_add_zero_r in p. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes