# On partial functions

Complete the following development:
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

You may use the `caseEq` tactic (page 160)
## Solution

Look at this file

Going home

Pierre Castéran