proposition: Theorem half_upper_bound : forall n, 2 * half n <= n.
proof: Proof. intros. destruct (half_double n) as [E|E]; rewrite E at 2. - apply le_refl. - nzsimpl. apply le_le_succ_r, le_refl. Qed.
imports: Bool RelationPairs NStrongRec