fact: Fixpoint update_primes (k:nat) (l: list (nat*nat)) {struct l} : list (nat*nat)*bool := match l with | nil => (nil,false) | (p,n)::tl => let (l',b) := update_primes k tl in match Nat.compare k n with | Lt => ((p, n)::l', b) | Eq => ((p, n+p)::l', true) | Gt => ((p, n+p)::l', b) end end.
imports: List Arith