proposition: Lemma CNFB_expos_zero: CNFB_expos \0o = emptyset.
proof: Proof. rewrite /CNFB_expos (the_CNF_p1 bg2) /cnf_exponents. by rewrite/domain/range funI_set0 funI_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)