proposition: Lemma char_fun_sub A A' B: sub A B -> sub A' B -> ((sub A A') <-> (forall x, inc x B -> (Vf (char_fun A B) x) <=c (Vf (char_fun A' B) x))).
proof: Proof. move=> AB A'B; split. move => AA' x xB; case: (inc_or_not x A) => xA. rewrite char_fun_V_a // char_fun_V_a //;[ fprops | by apply: AA']. rewrite char_fun_V_b //; last by apply /setC_P. by apply: cle0x; apply: char_fun_V_cardinal. move=> h t tA; ex_middle ta'; move: (AB _ tA) => tB. move: (h _ tB); rewrite char_fun_V_a // char_fun_V_b //; last by apply /setC_P. by move /(cltNge clt_01). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)