proposition: Lemma dnf_to_form_qf bcs : qf_form (odnf_to_oform bcs).
proof: Proof. elim: bcs => //= [[clT clF] clLt clLe ? ->] /=; elim: clT => //=. by rewrite andbT; elim: clF; elim: clLt => //; elim: clLe. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div choice fintype) mathcomp(bigop order ssralg finset fingroup zmodp) mathcomp(poly ssrnum)