proposition: Theorem half_double : forall n, n == 2 * half n \/ n == 1 + 2 * half n.
proof: Proof. intros. unfold half. nzsimpl'. destruct (half_aux_spec2 n) as [H|H]; [left|right]. - rewrite <- H at 1. apply half_aux_spec. - rewrite <- add_succ_l. rewrite <- H at 1. apply half_aux_spec. Qed.
imports: Bool RelationPairs NStrongRec