proposition: Lemma canon_proj_diagonal_fb x: bijection (canon_proj (diagonal x)).
proof: Proof. have [h sr] :=(diagonal_equivalence x). have cps:= (canon_proj_fs h). split => //; split;first by fct_tac. aw; move=> a b ax bx /=. rewrite !canon_proj_V //. move: ax bx;rewrite sr => ax bx. rewrite ! diagonal_class //; apply:set1_inj. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)