proposition: Fact prime_ge_2 p : prime p -> 2 <= p.
proof: Proof. destruct p as [ | [ | p ] ]; try lia. + intros [ _ H ]; subst. destruct (H 2); auto; discriminate. + intros [ [] _ ]; auto. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)