proposition: Lemma ldomUn h1 h2 : ldom (h1 :+ h2) =i [pred x | def (h1 :+ h2) && (x \in [predU ldom h1 & ldom h2])].
proof: Proof. by move=>x; rewrite !inE !ldomP domUn !inE /= -andbA andb_orl. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep