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