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