proposition: Lemma charfun_simplr b A B : (fun x => charfun A (b :: B) (x.1, b :: x.2)) == charfun A B.
proof: Proof. Proof using. move => [X Y] /=. by rewrite /charfun /eq_op /= {2}/eq_op /= eq_refl. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure