proposition: Lemma constant_function_pr2 x h: inc x (source h) -> constantfp h -> exists g f, [/\ g \coP f, h = g \co f, surjection f & singletonp (target f)].
proof: Proof. move=> xs [fh p]; set (y := Vf h x). have ssyth: sub (singleton y) (target h) by apply:set1_sub; rewrite /y; fprops. have ysy: inc y (singleton y) by fprops. set (g:= canonical_injection (singleton y) (target h)); exists g. set (f:= constant_function (source h) (singleton y) y); exists f. have ff: function f by apply: constant_f. have tf: target f = (singleton y) by rewrite constant_t. have sf: source f = source h by rewrite constant_s. have tg: target g = target h by rewrite /g /canonical_injection; aw. have sg: source g = singleton y by rewrite /g /canonical_injection; aw. have cop: g \coP f by rewrite /g;split; fprops; rewrite tf. split => //. - apply: function_exten;aw; fprops; try fct_tac. move=> z zh; rewrite compfV //; last ue. by rewrite (p _ _ zh xs) /f constant_V // ci_V. - split=>//; rewrite sf tf; move =>z /set1_P ->. by exists x; rewrite ?sf ?constant_V. - by rewrite tf; exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)