proposition: Lemma constant_prop1 f: constantgp f -> small_set (range f).
proof: Proof. move=> [ff eq] t1 t2 /(range_gP ff) [x xd ->] /(range_gP ff) [y yd ->]. by apply: eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)