proposition: Lemma unA : forall h1 h2 h3, h1 :+ (h2 :+ h3) = h1 :+ h2 :+ h3.
proof: Proof. case=>[|h1 H1]; case=>[|h2 H2]; case=>[|h3 H3] //; rewrite /union2; case: ifP=>//; case: ifP=>//; last first. - by move=>E1 E2; rewrite disjC disj_fcat andbC disjC E2. - by case: ifP=>E1 //; rewrite disj_fcat E1 /= -!(disjC h3) disj_fcat=>->->. rewrite disj_fcat; case/andP=>->. rewrite -!(disjC h3) disj_fcat=>E2 E3. by rewrite E2 E3 -heapE fcatA // disjC. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep