proposition: Lemma constant_prop4 f: function f -> (constantfp f <-> small_set (Imf f)).
proof: Proof. move => ff; split => h. rewrite (ImfE ff). by apply: constant_prop1; apply: constant_prop2. split=> // x x' xs x's; apply: h; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)