proposition: Lemma char_fun_setU A A' B x: sub A B -> sub A' B -> inc x B -> (Vf (char_fun (A \cap A') B) x) +c (Vf (char_fun (A \cup 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. have Hb:sub (A \cup A') B by move=> t /setU2_P; case; fprops. case: (p_or_not_p (inc x A))=> xA. rewrite (char_fun_V_a AB xA). rewrite (char_fun_V_a Hb (setU2_1 A' xA)). case: (p_or_not_p (inc x A'))=> xA'. by rewrite (char_fun_V_a A'B xA') char_fun_V_a //; apply: setI2_i. rewrite csumC; apply: f_equal. by rewrite ! char_fun_V_b //; apply /setC_P; split => //; move /setI2_P => []. have Hc: inc x (B -s A) by fprops. have Hd:inc x (B -s (A \cap A')). by apply /setC_P; split => //; move /setI2_P => []. rewrite (char_fun_V_b AB Hc) (char_fun_V_b Ha Hd). case: (p_or_not_p (inc x A')) => aux. have xu: inc x (A \cup A') by apply: setU2_2. by rewrite (char_fun_V_a Hb xu) (char_fun_V_a A'B aux). have xc:inc x (B -s (A \cup A')). by apply /setC_P; split => //;move /setU2_P => []. have xba: inc x (B -s A') by fprops. by rewrite (char_fun_V_b Hb xc) (char_fun_V_b A'B xba). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)