proposition: Lemma g_domain : forall n, P (n+2) <-> g n <> None.
proof: Proof. unfold g; intro n; case (f_domain (n+2)); intros H1 H2. split; intro H; case_eq (f (n+2)) . - discriminate. - intro H3; now destruct (H1 H). - intros n0 H3; apply H2; rewrite H3; discriminate. - intro H3; rewrite H3 in H; now destruct H. Qed.