proposition: Fact div_rem_mult n : div n (p*q) = div (div n p) q /\ rem n (p*q) = rem n p + p*rem (div n p) q.
proof: Proof. Proof using Hp Hq. assert (p*q <> 0) as Hpq. { intros E; apply Nat.eq_mul_0 in E; lia. } apply div_rem_uniq with (p := p*q); auto. + generalize (div_rem_spec1 n p) (div_rem_spec1 (div n p) q) (div_rem_spec1 n (p*q)); intros H1 H2 H3. rewrite <- H3; rewrite H1 at 1; rewrite H2 at 1; ring. + apply div_rem_spec2; auto. + generalize (div_rem_spec2 n Hp) (div_rem_spec2 (div n p) Hq); intros H1 H2. replace q with (1+(q-1)) at 2 by lia. rewrite Nat.mul_add_distr_l. apply Nat.add_lt_le_mono; try lia. apply Nat.mul_le_mono; lia. Qed.
imports: Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat gcd sums pos vec)