proposition: Theorem div_mult_comp: forall n m p, 0 < p -> div (p * m + n) p = m + div n p.
proof: Proof. intros n m p H0. apply lexico_mult with (b := p) (c1 := mod (p * m + n) p) (c2 := mod n p); try apply mod_lt; auto with arith. rewrite Nat.mul_add_distr_r, <- Nat.add_assoc; repeat rewrite <- div_mod_correct; auto with arith. Qed.
imports: Arith Tactic Psatz