proposition: Lemma per_add_edge_symmetric : forall A (B : binary A) x y, per_add_edge B y x = per_add_edge B x y.
proof: Proof. Proof using. unfold per_add_edge. intros. do 2 rewrite <- tclosure_sclosure_eq_stclosure. f_equal. apply pred_ext_2. intros a b. do 2 rewrite sclosure_eq. unfold Rel.union, per_single. tauto. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibRelation LibContainer LibSet)