proposition: Lemma union_quot_rEl (x: S): union_quot_r (inl x) = \pi (inl x).
proof: Proof. simpl. by rewrite union_quot_lEr quot_bijE. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)