proposition: Lemma quo_rel_pr s t (r := inv_image_relation (canon_proj s) t): equivalence s -> equivalence t -> substrate t = quotient s -> t = quotient_of_relations r s.
proof: Proof. move=> es et st. have iaa: iirel_axioms (canon_proj s) t. by split;aww. have [er sr]:=(iirel_relation iaa). have fa:finer_axioms s r. by split=>//; rewrite /r sr //; aw. have fe: finer_equivalence s r. move => x y sxy; apply / iirel_relatedP => //. have xs: inc x (substrate s) by substr_tac. have ys: inc y (substrate s) by substr_tac. aw; rewrite !canon_proj_V//; split=>//. have -> : (class s x =class s y) by apply: class_eq1. by apply: reflexivity_e=>//; rewrite st; fprops. have [eq sr'] := (quo_rel_equivalence fa fe). apply/sgraph_exten; fprops. move=> u v; split. move => tuv; apply/quo_rel_relatedP => //. have us: (inc u (quotient s)) by rewrite - st; substr_tac. have vs: (inc v (quotient s)) by rewrite - st; substr_tac. have rus: (inc (rep u) (substrate s)) by fprops. have rvs: (inc (rep v) (substrate s)) by fprops. split=>//; apply /iirel_relatedP => //. by aw;split; trivial; rewrite !canon_proj_V// !class_rep //. move/(quo_rel_relatedP fa fe) => [uq vq]. move /(iirel_relatedP iaa) ;rewrite canon_proj_s. by move=> [ru rv]; rewrite !canon_proj_V// ! class_rep. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)