proposition: Lemma odnf_to_oform_cat e c d : holds e (odnf_to_oform (c ++ d)) <-> holds e ((odnf_to_oform c) \/ (odnf_to_oform d))%oT.
proof: Proof. elim: c d => [| tc c ihc] d /=; first by split => // hd; [right | case: hd]. rewrite ihc /=; split. case; first by case=> ?; case=> ?; case=> ? ?; left; left. case; first by move=> ?; left; right. by move=> ?; right. case; last by move=> ?; right; right. case; last by move=> ?; right; left. by do 3!case=> ?; move=> ?; left. 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)