proposition: Theorem test_odds_correct : forall (n x:nat)(p:Z), p = 2*(Z_of_nat n)+1 -> (1 < x)%nat -> test_odds n p (Z_of_nat x) = true -> forall q:nat, (1 < q <= 2*n+1)%nat -> ~(exists y:nat, x = q*y)%nat.
proof: Proof. induction n. - intros x p Hp1 H1ltx Hn q Hint. exfalso; lia. - intros x p Hp H1ltx; simpl (test_odds (S n) p (Z_of_nat x)); intros Htest q (H1ltq, Hqle). case_eq (test_odds n (p -2) (Z_of_nat x)). + intros Htest'true. rewrite Htest'true in Htest. unfold divides_bool in Htest. elim (proj1 (Nat.lt_eq_cases q (2*S n + 1)%nat) Hqle). * intros Hqlt. assert (Hqle': (q <= (2* S n))%nat) by lia. elim (proj1 (Nat.lt_eq_cases q (2 * S n)%nat) Hqle'). replace (2*S n)%nat with (2*n +2)%nat. intros Hqlt'. assert (Hqle'' : (q <= 2*n +1)%nat) by lia. apply (IHn x (p - 2)); auto with zarith arith; try (rewrite Hp; rewrite inj_S; unfold Z.succ); ring. ring. intros Hq (y, Hdiv); elim (test_odds_correct2 n x H1ltx (p - 2)); auto. exists (S n * y)%nat; rewrite Hdiv; rewrite Hq; ring. * intros Hq Hex; assert (Hp' : p = Z_of_nat q). rewrite Hp; rewrite Hq; rewrite inj_plus; rewrite inj_mult; auto. rewrite Hp' in Htest; rewrite (verif_divide x q) in Htest. simpl in Htest; discriminate. lia. lia. elim Hex; intros y Hdiv; exists y; rewrite Hdiv; ring. + intros Htest'; rewrite Htest' in Htest; simpl in Htest; discriminate. Qed.
imports: ZArith Arith Bool Lia