proposition: Fact prime_algo p : prime p <-> p = 2 \/ 3 <= p /\ ~ 2 <d p /\ forall n, 3+2*n < p -> ~ 3+2*n <d p.
proof: Proof. split. + intros (H1 & H2). destruct (le_lt_dec 3 p) as [ H | H ]. * right; split; auto; split. - intros H3; apply H2 in H3; lia. - intros n Hn C; apply H2 in C; lia. * left; destruct p as [ | [ | [ | p ] ] ]; try lia. destruct (H2 2); try lia. exists 0; auto. + intros [ H1 | (H1 & H2 & H3) ]. * subst; auto. * split; try lia. intros q Hq. destruct (euclid_2 q) as (k & [ H4 | H4 ]). - destruct H2; apply divides_trans with (2 := Hq). exists k; lia. - destruct k; try lia. destruct (le_lt_dec p (3+2*k)) as [ H5 | H5 ]. ++ apply divides_le in Hq; lia. ++ destruct (H3 k); auto. eq goal Hq; f_equal; lia. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)