proposition: Lemma Exercise1_3a10: (fun_on_quotient E13_S E13_lam) \coP (canon_proj E13_S).
proof: Proof. split => //; first by apply: Exercise1_3a9. apply: canon_proj_f; apply: Exercise1_3a7. by rewrite /fun_on_quotient/section_canon_proj; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)