proposition: Theorem neq_0_lt_0 : forall n, n ~= 0 <-> 0 < n.
proof: Proof. intro n; cases n. - split; intro H; [now elim H | intro; now apply lt_irrefl with 0]. - intro n; split; intro H; [apply lt_0_succ | apply neq_succ_0]. Qed.
imports: NAdd