proposition: Lemma trichotomy_preserved : forall R R' x y, R << R' -> trichotomy R x y -> trichotomy R' x y.
proof: Proof. unfold inclusion, trichotomy. intros. pose (H x y). pose (H y x). tauto. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)