proposition: Theorem prime_rect n : P n.
proof: Proof. Proof using HP0 HP1 HPp HPm. induction on n as IHn with measure n. destruct n as [ | [ | n ] ]; auto. destruct (@prime_factor (S (S n))) as (p & H1 & H2); try lia. apply divides_div in H2. rewrite H2. apply HPm. + apply IHn. rewrite H2 at 2. rewrite <- Nat.mul_1_r at 1. apply prime_ge_2 in H1. apply Nat.mul_lt_mono_pos_l; lia. + apply HPp, H1. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)