proposition: Lemma try_add_arc_trichotomy : eq_midex A -> rel_midex R -> forall x y, trichotomy (try_add_arc x y) x y.
proof: Proof. unfold trichotomy. intros. destruct (H x y). tauto. destruct (H0 x y). do 2 constructor. hyp. destruct (H0 y x). do 2 constructor 2. constructor. hyp. constructor. constructor 2; hyp. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)