proposition: Lemma trans_try_add_arc_sym : forall x y z t, transitive R -> try_add_arc x y z t -> try_add_arc x y t z -> R z z.
proof: Proof. unfold transitive. intros. apply H with t; apply try_add_arc_sym with x y; hyp. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)