proposition: Lemma independent_sym (p q : Path x y): independent p q -> independent q p.
proof: Proof. by rewrite /independent disjoint_sym. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)