fact: Fixpoint prime_sieve (n:nat) : list (nat*nat) := match n with | O => nil | 1 => nil | S k' => let (l', b) := update_primes (S k')(prime_sieve k') in if b then l' else ((S k', 2*S k')::l') end.
imports: List Arith