proposition: Theorem zero_one : forall n, n == 0 \/ n == 1 \/ 1 < n.
proof: Proof. setoid_rewrite one_succ. intro n; induct n. { now left. } intro n; cases n. { intros; right; now left. } intros n IH. destruct IH as [H | [H | H]]. - false_hyp H neq_succ_0. - right; right. rewrite H. apply lt_succ_diag_r. - right; right. now apply lt_lt_succ_r. Qed.
imports: NAdd