Sf.v

(* compile with Coq 8.4pl2 *)
Fixpoint evenb (n:nat) : bool :=                                                                                
  match n with                                                                                                  
  | O => true                                                                                                   
  | S O => false                                                                                                
  | S (S n') => evenb n'                                                                                        
  end.                                                                                                          

Definition negb (b:bool) : bool :=                                                                              
  match b with                                                                                                  
  | true => false                                                                                               
  | false => true                                                                                               
  end.                                                                                                          


Definition oddb (n:nat) : bool := negb (evenb n).