proposition: Theorem half_decrease : forall n, 0 < n -> half n < n.
proof: Proof. intros n LT. destruct (half_double n) as [E|E]; rewrite E at 2; nzsimpl'. - rewrite <- add_0_l at 1. rewrite <- add_lt_mono_r. assert (LE : 0 <= half n) by apply le_0_l. le_elim LE; auto. rewrite <- LE, mul_0_r in E. rewrite E in LT. destruct (nlt_0_r _ LT). - rewrite <- add_succ_l. rewrite <- add_0_l at 1. rewrite <- add_lt_mono_r. apply lt_0_succ. Qed.
imports: Bool RelationPairs NStrongRec