proposition: Lemma per_add_edge_le : forall A (B:binary A) a b, rel_incl B (per_add_edge B a b).
proof: Proof. Proof using. introv. intros x y H. apply stclosure_once. left~. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibRelation LibContainer LibSet)