proposition: Lemma eqv_clot_LR (T1 T2 : finType) (x : T1) (y : T2) o i : inl T2 x = inr T1 y %[mod eqv_clot [:: (inl o,inr i)]] -> x = o /\ y = i.
proof: Proof. move/eqquotP. by case/eqv_clot1E => [//|[[->][->]]|[//]]. Qed.
imports: Coq(RelationClasses Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij finite_quotient)