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