proposition: Theorem test_odds_correct2 : forall n x:nat, (1 < x)%nat -> forall p:Z, test_odds n p (Z_of_nat x) = true -> ~(exists y:nat, x = y*2)%nat.
proof: Proof. intros n; elim n. - unfold test_odds, divides_bool; intros x H1ltx _ Heq Hex. assert (Heq' : Z_of_nat x mod Z_of_nat 2 = 0). + apply verif_divide; auto with zarith. + simpl (Z_of_nat 2) in Heq'; rewrite Heq' in Heq; simpl in Heq; discriminate. - clear n; intros n IHn x H1ltx p; simpl. case_eq (test_odds n (p - 2) (Z_of_nat x)). + intros Htest' _ ; apply (IHn x H1ltx (p -2)); auto. + intros; discriminate. Qed.
imports: ZArith Arith Bool Lia