proposition: Lemma subdomD h1 h2 h : subdom h1 h2 -> def (h2 :+ h) -> def (h1 :+ h).
proof: Proof. case: h1 h2 h=>[|h1 H1] [|h2 H2] [|h H] //=. rewrite /subdom /def /union2 /=; case: ifP=>E1 //; case: ifP=>E2 // E _. case: disjP E2=>// x H3 H4 _; case: disjP E1=>// X1 _. by case: (allP (s := supp h1)) E=>//; move/(_ _ H3); move/X1; rewrite H4. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep