proposition: Lemma per_add_edge_per : forall A (R : binary A) a b, per R -> per (per_add_edge R a b).
proof: Proof. Proof using. introv [Rs Rt]. unfold per_add_edge. constructor. introv H. applys~ sym_stclosure. applys~ trans_stclosure. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibRelation LibContainer LibSet)