proposition: Fact div_rem_spec1 q p : q = div q p * p + rem q p.
proof: Proof. apply (proj2_sig (projT2 (div_full q p))). Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)