proposition: Lemma char_fun_constant A B: sub A B -> (cstfp (char_fun A B) B) -> (A=B \/ A = emptyset).
proof: Proof. move=> AB p. case: (emptyset_dichot A); [by right | move=> [u uA]; left ]. apply: extensionality=>// t tB. ex_middle v;case: card1_nz. move: (p u t (AB _ uA) tB). rewrite (char_fun_V_a AB uA) (char_fun_V_b AB) //. by apply /setC_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)