proposition: Lemma union_quot_rEr (x: T): union_quot_r (inr (\pi x)) = \pi (inr x).
proof: Proof. simpl. by rewrite union_quot_lEl quot_bijE. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)