proposition: Lemma char_fun_setC A B x: sub A B -> inc x B -> Vf (char_fun (B -s A) B) x = \1c -c (Vf (char_fun A B) x).
proof: Proof. move=> AB xB. have sc:= (@sub_setC B A). case: (inc_or_not x A) => xA. rewrite char_fun_V_b ? setC_K //. by rewrite char_fun_V_a // (cdiff_nn). move/setC_P: (conj xB xA) => xc. by rewrite char_fun_V_a // char_fun_V_b // (cdiff_n0 NS1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)