proposition: Lemma char_fun_V_b A B x: sub A B -> inc x (B -s A) -> Vf (char_fun A B) x = \0c.
proof: Proof. move=> AB /setC_P [xB nxA]; rewrite (char_fun_V _ xB). by apply: varianti_out. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)