proposition: Theorem half_nz : forall n, 1 < n -> 0 < half n.
proof: Proof. intros n LT. assert (LE : 0 <= half n) by apply le_0_l. le_elim LE; auto. destruct (half_double n) as [E|E]; rewrite <- LE, mul_0_r, ?add_0_r in E; rewrite E in LT. - order'. - order. Qed.
imports: Bool RelationPairs NStrongRec