proposition: Lemma empUn h1 h2 : empb (h1 :+ h2) = empb h1 && empb h2.
proof: Proof. case: h1 h2=>[|h1 H1] // [|h2 H2] /=; first by rewrite andbC. rewrite /empb /union2; case: ifP=>E; case: eqP=>E1; case: eqP=>E2 //=; last 2 first. - by move: E2 E1; move/supp_nilE=>->; rewrite fcat0s; case: eqP. - by move: E1 E2 E; do 2![move/supp_nilE=>->]; case: disjP. - by move/supp_nilE: E2 E1=>-> <-; rewrite fcat0s eq_refl. have [k H3]: exists k, k \in supp h1. - case: (supp h1) {E1 H1 E} E2=>[|x s _] //. by exists x; rewrite inE eq_refl. suff: k \in supp (fcat h1 h2) by rewrite E1. by rewrite supp_fcat inE /= H3. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep