fact: Fixpoint test_odds (n:nat) (p t:Z) {struct n} : bool := match n with | 0%nat => negb (divides_bool 2 t) | S n' => if test_odds n' (p - 2) t then negb (divides_bool p t) else false end.
imports: ZArith Arith Bool Lia