proposition: Lemma Exercise1_3a9: function (fun_on_quotient E13_S E13_lam).
proof: Proof. move: Exercise1_3a0 => aux. move:Exercise1_3a3'' => [sa sb]. by apply: foqc_f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)