proposition: Lemma cnv_inj x y: x° ≡ y° -> x ≡ y.
proof: Proof. intro. rewrite <-(cnvI x), <-(cnvI y). by apply cnv_eqv. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop structures)