proposition: Lemma subheap_trans h2 h1 h3 : subheap h1 h2 -> subheap h2 h3 -> subheap h1 h3.
proof: Proof. move=>[S12 E12] [S23 E23]. split=> [|x in1]; first by apply: (subdom_trans S12 S23). by rewrite (E12 x in1); apply: (E23 x (subdomQ S12 in1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep