proposition: Lemma function_exten4 f g: source f = source g -> surjection f -> surjection g -> {inc source f, f =1f g} -> f = g.
proof: Proof. move=> sfg sf sg Weq. have ff: function f by fct_tac. have fg: function g by fct_tac. have geq: (graph f = graph g). by apply: fgraph_exten; fprops; rewrite ! domain_fg. apply: function_exten1 => //. by rewrite -(surjective_pr0 sf) -(surjective_pr0 sg) !ImfE// geq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)