Lemma lt_neq_0 : forall n, 0 <> n -> 0 < n.
