proposition: Lemma add_edge_transp_geq : forall x, transpose geq (add_edge x).
proof: Proof. intros x y z g. unfold geq. rewrite !rel_add_edge. unfold same, inclusion, id, Relation_Operators.union. tauto. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)