proposition: Lemma canon_proj_fs: surjection (canon_proj r).
proof: Proof. split;[ fprops | move=> y; aw => yr; exists (rep y); fprops]. by rewrite (canon_proj_V (rep_i_sr er yr)) (class_rep er yr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)