proposition: Lemma cqr_aux s x y u: equivalence s -> sub y (substrate s) -> x = Vfs (canon_proj s) y -> (inc u x <-> (exists2 v, inc v y & u = class s v)).
proof: Proof. move=> es ys xi. split. rewrite xi /Vfs => ui. move:(sub_im_canon_proj_quotient ys ui) => uqs. move: ui=> /dirim_P [z zy Jg]; move : (ys _ zy) => zs. move: Jg => /(rel_gcp_P es zs uqs) zu. ex_tac. have aux: (class s (rep u) = u) by (apply: class_rep). have : related s (rep u) z by apply /(class_P es); ue. move /(related_equiv_P es) => [_ _]; ue. have fc: function (canon_proj s) by fprops. move=> [v vy ->]; move: (ys _ vy) => vs; rewrite xi. apply/dirim_P; ex_tac; apply /(rel_gcp_P es vs); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)