On partial functions

Section partial_functions.

 Variable P : nat -> Prop.
 Variable f : nat -> option nat.
 
 Hypothesis f_domain : forall n, P n <-> f n <> None.

 Definition g n : option nat := 
     match f (n+2) with None => None 
                      | Some y => Some (y + 2) end.


 Lemma g_domain : forall n, P (n+2) <-> g n <> None.
 ...
 Qed.
 
End partial_functions.

Hint

Solution