proposition: Fact compl_rel_sym : symmetric compl_rel.
proof: Proof. by move=> x y; rewrite /= eq_sym sgP. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)