fact: Fixpoint check_postulate (n : nat) : bool := match n with | O => true | S n1 => match n1 with | O => true | S n2 => match prime_between (S n) n2 with | true => check_postulate n1 | false => false end end end.
imports: Coq(Arith)