proposition: Lemma sub_im_canon_proj_quotient a x: sub a (substrate r) -> inc x (Vfs (canon_proj r) a) -> inc x (quotient r).
proof: Proof. move=> sas xi. have fc:function (canon_proj r) by fprops. have sa: sub a (source (canon_proj r)) by aw. move /(Vf_image_P fc sa): xi => [u ua ->]; rewrite (canon_proj_V); fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)