proposition: Lemma lt_empty_r : forall s s', Empty s' -> ~ lt s s'.
proof: Proof. intros s s' Hs' (x & _ & [(IN,_)|(_ & y & IN & _)]). - elim (Hs' x IN). - elim (Hs' y IN). Qed.
imports: Bool SetoidList RelationClasses Morphisms RelationPairs Equalities Orders OrdersFacts