Fixpoint D [n:nat] : nat :=
Cases n of O => O
    | (S p) => (S(S(D p)))
end.

Inductive even : nat -> Prop :=
  e0 : (even O)
| eS : (n:nat)(even n)->(even (S(S n))).



(* division : non-computational version *)

Lemma div_prop : (n:nat)(even n)->
                   (EX p:nat | n=(D p)).
Intros n en.
Elim en.
Simpl ; Exists O ; Reflexivity.
Intros n' en' [p hp].
Exists (S p) ; Simpl.
Rewrite hp ; Reflexivity.
Qed.


(* Computational version *)

Lemma div_c : (n:nat)(even n)->{p:nat | n=(D p)}.

Fix 1.
Destruct n.
Simpl; Split with O; Reflexivity.

Destruct n0.
Intro hh; Split with O; Inversion hh.

Intros n1 en1; Elim (div_c n1).
Intros x ex; Split with (S x).
Simpl.
Rewrite ex; Auto.

Inversion en1.
Auto.

Qed.


Extraction div_c.