proposition: Lemma n_modulo_2 : forall n:nat, {p | (n = 2 * p)%nat} + {p | n = S (2 * p)}.
proof: Proof. intro n ; induction n. left ; exists O ; intuition. case IHn ; intro H ; destruct H as (p,Hp) ; [right ; exists p | left ; exists (S p)] ; intuition (auto with arith); rewrite Hp; simpl; eauto with *. Qed.
imports: Reals