proposition: Lemma char_fun_setI A A' B x: sub A B -> sub A' B -> inc x B -> Vf (char_fun (A \cap A') B) x = (Vf (char_fun A B) x) *c (Vf (char_fun A' B) x).
proof: Proof. move=> AB A'B xB. have Ha:sub (A \cap A') B by move=> t /setI2_P [tA _]; apply: AB. case: (inc_or_not x A) => h. have cW:cardinalp (Vf (char_fun A' B) x) by apply: char_fun_V_cardinal. rewrite (char_fun_V_a AB h) cprod1l //. case: (inc_or_not x A') => xA. have aux:inc x (A \cap A') by apply: setI2_i. rewrite char_fun_V_a // char_fun_V_a //. have aux:inc x (B -s (A \cap A')) by apply /setC_P;split => //; move /setI2_P =>[_]. by rewrite char_fun_V_b // char_fun_V_b //; apply /setC_P. have aux: inc x (B -s (A \cap A')) by apply /setC_P;split => //; move /setI2_P =>[]. have aux2:inc x (B -s A) by fprops. by rewrite char_fun_V_b // char_fun_V_b // cprod0l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)