proposition: Fact div_by_p_lt p n : 2 <= p -> n <> 0 -> div n p < n.
proof: Proof. intros H1 H2. rewrite (div_rem_spec1 n p) at 2. replace p with (2+(p-2)) at 3 by lia. rewrite Nat.mul_add_distr_l. generalize (div n p*(p-2)); intros x. destruct (le_lt_dec p n) as [ Hp | Hp ]. + apply div_ge_1 in Hp; lia. + rewrite rem_lt; lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)