proposition: Lemma Exercise1_3a11: E13_lam = (fun_on_quotient E13_S E13_lam) \co (canon_proj E13_S).
proof: Proof. apply: (canonical_decomposition_surj2 Exercise1_3a2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)