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