x y q u (H : u <= y) : let (q', u') := nat_div_mod x y q u in x + y.+1 * q + (y - u) = y.+1 * q' + (y - u') /\ u' <= y. Proof. intros d r. induction x as [|x IHx] in y, q, u, H, d, r |- *; only 1: by split. destruct u as [|u]. - destruct (IHx y q.+1 y _) as [p H']. split; trivial. rewrite <- p, nat_sub_zero_r, nat_sub_cancel, nat_add_zero_r. simpl. by rewrite nat_add_succ_r, <- 2 nat_add_assoc, nat_mul_succ_r. - destruct (IHx y q u _) as [p H']. split; trivial. rewrite <- p, 2 nat_add_succ_l, <- nat_add_succ_r. snrapply ap. rewrite nat_sub_succ_r. apply nat_succ_pred. rapply lt_moveL_nV. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes