proposition: Lemma constant_constant_fun A B y: inc y B -> constantfp (constant_function A B y).
proof: Proof. split; first by apply: constant_f. rewrite constant_s => u v /= us vs; do 2 rewrite constant_V=>//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)