proposition: Lemma add_edge_already : forall A (B:binary A) a b, per B -> B a b -> per_add_edge B a b = B.
proof: Proof. Proof using. introv P H. extens. intros x y. iff M. induction M. destruct H0. auto. destruct H0. subst~. apply* per_sym. apply* per_trans. hnf in M. apply~ per_add_edge_le. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibRelation LibContainer LibSet)