proposition: Fact rem_prop q p n r : q = n*p+r -> r < p -> rem q p = r.
proof: Proof. intros H1 H2. apply (@div_rem_uniq p (div q p) _ n r); auto. + lia. + rewrite <- H1; symmetry; apply div_rem_spec1. + apply div_rem_spec2; lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)