proposition: Lemma not_try_add_arc : rel_midex R -> forall x y, x<>y -> ~try_add_arc x y x y -> R y x.
proof: Proof. intros. destruct (H y x). hyp. absurd (try_add_arc x y x y). hyp. constructor 2; hyp. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)