diff --git a/README.md b/README.md
index 943ea27..e6faa1f 100644
--- a/README.md
+++ b/README.md
@@ -20,7 +20,7 @@ Besides Mathcomp, this also requires the [Equations](https://mattam82.github.io/
 10. [Beyond Insert and Delete: \cup, \cap and -](src/beyond.v)
 11. [Arrays via Braun Trees](src/braun.v)
 12. [Tries](src/trie.v)
-13. Huffman’s Algorithm
+13. [Huffman’s Algorithm](src/huffman.v)
 ### Part III: Priority Queues
 14. Priority Queues
 15. Leftist Heaps
diff --git a/_CoqProject b/_CoqProject
index eef337a..01b469c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -14,4 +14,5 @@ src/redblack.v
 src/avl.v
 src/beyond.v
 src/braun.v
-src/trie.v
\ No newline at end of file
+src/trie.v
+src/huffman.v
\ No newline at end of file
diff --git a/src/huffman.v b/src/huffman.v
new file mode 100644
index 0000000..efb1c80
--- /dev/null
+++ b/src/huffman.v
@@ -0,0 +1,1727 @@
+From Equations Require Import Equations.
+From Coq Require Import ssreflect ssrbool ssrfun.
+From mathcomp Require Import eqtype ssrnat seq bigop ssrAC.
+From favssr Require Import prelude.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Section TheImplementation.
+Context {A : Type}.
+
+(* TODO most of forest functions (fooF) here can probably be rewritten as maps/folds *)
+
+Inductive tree A := Leaf of nat & A | Node of nat & tree A & tree A.
+
+Definition forest A := seq (tree A).
+
+Definition cachedWeight (t : tree A) : nat :=
+  match t with
+  | Leaf w _   => w
+  | Node w _ _ => w
+  end.
+
+Definition uniteTrees (l r : tree A) : tree A :=
+  Node (cachedWeight l + cachedWeight r) l r.
+
+Fixpoint insortTree (u : tree A) (ts : forest A) : forest A :=
+  if ts is t::s then
+    if cachedWeight u <= cachedWeight t
+      then u :: t :: s
+      else t :: insortTree u s
+  else [::u].
+
+Lemma size_insortTree u ts : size (insortTree u ts) = (size ts).+1.
+Proof. by elim: ts=>//=t s IH; case: ifP=>//= _; rewrite IH. Qed.
+
+Equations? huffman (t0 : tree A) (ts : forest A) : tree A by wf (size ts) lt :=
+huffman t0 [::]         => t0;
+huffman _  [::t]        => t;
+huffman t0 (t1::t2::ts) => huffman t0 (insortTree (uniteTrees t1 t2) ts).
+Proof. by apply: ssrnat.ltP; rewrite size_insortTree. Qed.
+
+End TheImplementation.
+
+Lemma insortTree_notnil {A} (p : tree A) ts:
+  ~~ nilp (insortTree p ts).
+Proof. by case: ts=>//=t s; case: ifP. Qed.
+
+Section EqTree.
+Context {T : eqType}.
+
+Fixpoint eqtree (t1 t2 : tree T) :=
+  match t1, t2 with
+  | Leaf w1 x1, Leaf w2 x2 => (w1 == w2) && (x1 == x2)
+  | Node w1 l1 r1, Node w2 l2 r2 => [&& w1 == w2, eqtree l1 l2 & eqtree r1 r2]
+  | _, _ => false
+  end.
+
+Lemma eqtreeP : Equality.axiom eqtree.
+Proof.
+move; elim=>[w1 x1|w1 l1 IHl r1 IHr][w2 x2|w2 l2 r2] /=; try by constructor.
+apply: (iffP andP).
+- by case=>/eqP->/eqP->.
+by case=>->->.
+have [<-/=|neqx] := w1 =P w2; last by apply: ReflectF; case.
+- apply: (iffP andP).
+- by case=>/IHl->/IHr->.
+by case=><-<-; split; [apply/IHl|apply/IHr].
+Qed.
+
+Canonical tree_eqMixin := EqMixin eqtreeP.
+Canonical tree_eqType := Eval hnf in EqType (tree T) tree_eqMixin.
+
+End EqTree.
+
+Section BasicAuxiliaryFunctions.
+Context {A : eqType}.
+
+(* alphabets & intersection *)
+
+Fixpoint alphabet (t : tree A) : pred A :=
+  match t with
+  | Leaf _ a => pred1 a
+  | Node _ l r => [predU (alphabet l) & (alphabet r)]
+  end.
+
+Lemma exists_in_alphabet t :
+  exists a, a \in alphabet t.
+Proof.
+elim: t=>/=[_ c|_ l IHl r _].
+- by exists c; exact: eq_refl.
+by case: IHl=>a Ha; exists a; rewrite !inE Ha.
+Qed.
+
+Fixpoint alphabetF (ts : forest A) : pred A :=
+  if ts is t::s then [predU (alphabet t) & (alphabetF s)]
+    else pred0.
+
+Fixpoint enum (t : tree A) : seq A :=
+  match t with
+  | Leaf _ a => [::a]
+  | Node _ l r => enum l ++ enum r
+  end.
+
+Fixpoint enumF (ts : forest A) : seq A :=
+  if ts is t::s then enum t ++ enumF s
+    else [::].
+
+Lemma alphabet_enum t : alphabet t =i enum t.
+Proof.
+elim: t=>[w a|w l IHl r IHr] /= z.
+- by rewrite in_cons in_nil orbF.
+by rewrite !inE mem_cat (IHl z) (IHr z).
+Qed.
+
+Lemma alphabet_enumF t : alphabetF t =i enumF t.
+Proof.
+elim: t=>//=t s IH z.
+by rewrite !inE mem_cat alphabet_enum IH.
+Qed.
+
+Lemma alphabetF_insortTree (p : tree A) ts :
+  alphabetF (insortTree p ts) =i [predU (alphabet p) & (alphabetF ts)].
+Proof.
+elim: ts=>//=t s IH; case: ifP=>//= _ x.
+by rewrite !inE IH !inE orbCA.
+Qed.
+
+Definition alpha_intersects p q := has (alphabet p) (enum q).
+
+Definition alpha_intersectsF p qs := has (alphabet p) (enumF qs).
+
+Lemma intersectsC p q : alpha_intersects p q = alpha_intersects q p.
+Proof.
+rewrite /alpha_intersects; elim: p=>/= _.
+- by move=>a; rewrite has_pred1 orbF -(alphabet_enum q).
+by move=>l IHl r IHr; rewrite has_predU has_cat IHl IHr.
+Qed.
+
+Lemma alpha_not p q :
+  ~~ alpha_intersects p q <->
+  (forall x, x \in alphabet p -> x \notin alphabet q).
+Proof.
+split.
+- move=>Hi x Hp; apply/negP; rewrite alphabet_enum=>Hq.
+  by move/hasPn: Hi=>/(_ x Hq); move: Hp; rewrite -topredE /==>->.
+move=>H; rewrite intersectsC /alpha_intersects; apply/hasPn=>z; rewrite -alphabet_enum.
+by move/H; rewrite -topredE /=.
+Qed.
+
+Lemma alpha_notF p q :
+  ~~ alpha_intersectsF p q <->
+  (forall x, x \in alphabet p -> x \notin alphabetF q).
+Proof.
+split.
+- move=>Hi x Hp; apply/negP; rewrite alphabet_enumF=>Hq.
+  by move/hasPn: Hi =>/(_ x Hq); move: Hp; rewrite -topredE /==>->.
+move=>H; rewrite /alpha_intersectsF; apply/hasPn=>z; rewrite -alphabet_enumF=>Hq.
+by apply/negP=>/H; rewrite Hq.
+Qed.
+
+Lemma alpha_notFC p q :
+  ~~ alpha_intersectsF p q <->
+  (forall x, x \in alphabetF q -> x \notin alphabet p).
+Proof.
+split.
+- by move=>Hi x; apply/contraL; move: x; apply/alpha_notF.
+move=>H; rewrite /alpha_intersectsF; apply/hasPn=>z; rewrite -alphabet_enumF.
+by apply: H.
+Qed.
+
+Lemma not_intersects p q x :
+  ~~ alpha_intersects p q ->
+  [\/ (x \in    alphabet p) /\ (x \notin alphabet q)
+    , (x \notin alphabet p) /\ (x \in    alphabet q)
+    | (x \notin alphabet p) /\ (x \notin alphabet q)
+  ].
+Proof.
+move=>Hi.
+case/boolP: (x \in alphabet p)=>Hp; case/boolP: (x \in alphabet q)=>Hq /=; try by constructor.
+by move/alpha_not: Hi=>/(_ _ Hp); rewrite Hq.
+Qed.
+
+Lemma alpha_intersectsF_cons (p : tree A) q ts :
+  alpha_intersectsF p (q::ts) = alpha_intersects p q || alpha_intersectsF p ts.
+Proof. by rewrite /alpha_intersects /alpha_intersectsF /= has_cat. Qed.
+
+Lemma alpha_intersectsF_uniteTrees (p : tree A) q ts :
+  alpha_intersectsF (uniteTrees p q) ts = alpha_intersectsF p ts || alpha_intersectsF q ts.
+Proof. by rewrite /alpha_intersectsF /uniteTrees /= has_predU. Qed.
+
+Lemma intersectsF_insortTree (p : tree A) q ts :
+  alpha_intersectsF p (insortTree q ts) = alpha_intersects p q || alpha_intersectsF p ts.
+Proof.
+rewrite /alpha_intersects /alpha_intersectsF; elim: ts=>/=.
+- by rewrite cats0 orbF.
+move=>t s IH; case: ifP=>/= _; rewrite !has_cat //.
+by rewrite IH orbCA.
+Qed.
+
+(* consistency *)
+
+Fixpoint consistent (t : tree A) : bool :=
+  if t is Node _ l r
+    then [&& ~~ alpha_intersects l r,
+             consistent l &
+             consistent r]
+    else true.
+
+Fixpoint consistentF (ts : forest A) : bool :=
+  if ts is t::s
+    then [&& ~~ alpha_intersectsF t s,
+             consistent t &
+             consistentF s]
+  else true.
+
+Lemma consistent_ind (P : tree A -> A -> Prop) t a:
+  consistent t ->
+  (forall w b a, P (Leaf w b) a) ->
+  (forall w l r a,
+     consistent l -> consistent r ->
+     ~~ alpha_intersects l r ->
+     a \in alphabet l -> a \notin alphabet r ->
+     P l a -> P r a ->
+     P (Node w l r) a) ->
+  (forall w l r a,
+     consistent l -> consistent r ->
+     ~~ alpha_intersects l r ->
+     a \notin alphabet l -> a \in alphabet r ->
+     P l a -> P r a ->
+     P (Node w l r) a) ->
+  (forall w l r a,
+     consistent l -> consistent r ->
+     ~~ alpha_intersects l r ->
+     a \notin alphabet l -> a \notin alphabet r ->
+     P l a -> P r a ->
+     P (Node w l r) a) ->
+  P t a.
+Proof.
+move=>Hc H0 Hl Hr Hb; elim: t Hc=>[w b|w l IHl r IHr] /=.
+- by move=>_; apply: H0.
+case/and3P=>Hi Hcl Hcr.
+case: (not_intersects a Hi); case=>Hil Hir.
+- by apply: Hl=>//; [apply: IHl|apply: IHr].
+- by apply: Hr=>//; [apply: IHl|apply: IHr].
+by apply: Hb=>//; [apply: IHl|apply: IHr].
+Qed.
+
+Lemma consistentF_insortTree (p : tree A) ts :
+  consistentF (insortTree p ts) = consistentF (p::ts).
+Proof.
+elim: ts=>//=t s IH; case: ifP=>//= _.
+rewrite intersectsF_insortTree IH alpha_intersectsF_cons !negb_or intersectsC.
+by rewrite !andbA (ACl (1*4*5*2*3*6)%AC).
+Qed.
+
+(* tree metrics *)
+
+Fixpoint depth (t : tree A) (a : A) : nat :=
+  if t is Node _ l r then
+    if a \in alphabet l
+      then depth l a + 1
+      else if a \in alphabet r
+        then depth r a + 1
+        else 0
+  else 0.
+
+Fixpoint height (t : tree A) : nat :=
+  if t is Node _ l r
+    then maxn (height l) (height r) + 1
+  else 0.
+
+Fixpoint heightF (ts : forest A) : nat :=
+  if ts is t::s
+    then maxn (height t) (heightF s)
+    else 0.
+
+Lemma heightE (t : tree A) : reflect (exists w x, t = Leaf w x) (height t == 0).
+Proof.
+apply: (iffP idP); last by case=>w[x]->.
+case: t=>[w x|w l r] /=; last by rewrite addn1.
+by move=>_; exists w, x.
+Qed.
+
+Lemma depth_le_height t a :
+  depth t a <= height t.
+Proof.
+elim: t=>//=_ l IHl r IHr; case: ifP=>_.
+- by rewrite leq_add2r leq_max IHl.
+case: ifP=>_.
+- by rewrite leq_add2r leq_max IHr orbT.
+by rewrite addn1.
+Qed.
+
+Lemma exists_at_height t :
+  consistent t -> exists2 a, a \in alphabet t & depth t a = height t.
+Proof.
+elim: t=>/=[_ a|_ l IHl r IHr].
+- move=>_; exists a=>//; apply: eq_refl.
+case/and3P=>Hi Hl Hr.
+case: (IHl Hl)=>al Hal Hdl.
+case: (IHr Hr)=>ar Har Hdr.
+case: (leqP (height r) (height l))=>H.
+- exists al; rewrite ?inE Hal //.
+  by rewrite Hdl.
+ exists ar; rewrite ?inE Har; first by rewrite orbT.
+ move: Hi; rewrite intersectsC=>/alpha_not/(_ _ Har)/negbTE->.
+ by rewrite Hdr.
+Qed.
+
+Lemma height_gt0_alphabet_eq t u :
+  0 < height t -> consistent t -> alphabet t =i alphabet u ->
+  0 < height u.
+Proof.
+case: t=>//=_ l r _; case/and3P=>Hi Hl Hr.
+case: (exists_in_alphabet l)=>b Hb.
+case: (exists_in_alphabet r)=>c Hc.
+case/boolP: (b==c).
+- move/eqP=>E; rewrite -E in Hc.
+  by move/alpha_not: Hi=>/(_ _ Hb); rewrite Hc.
+move=>Hbc; case: u=>/=[_ a|_ lu ru]; last by rewrite addn1.
+move=>H; move: (H b) (H c); rewrite !inE Hb Hc /= orbT => Hba Hca.
+symmetry in Hba; move/eqP: Hba=>Hba; rewrite -Hba in Hca.
+by symmetry in Hca; move/eqP: Hca=>Hca; rewrite Hca eq_refl in Hbc.
+Qed.
+
+Lemma heightF_insortTree (p : tree A) ts :
+  heightF (insortTree p ts) = maxn (height p) (heightF ts).
+Proof.
+elim: ts=>//= t s IH; case: ifP=>//= _.
+by rewrite IH maxnCA.
+Qed.
+
+Fixpoint freq (t : tree A) (b : A) : nat :=
+  match t with
+  | Leaf w a => if b == a then w else 0
+  | Node _ l r => freq l b + freq r b
+  end.
+
+Fixpoint freqF (ts : forest A) (b : A) : nat :=
+  if ts is t::s
+    then freq t b + freqF s b
+    else 0.
+
+Lemma notin_alphabet_freq_0 a t :
+  a \notin alphabet t -> freq t a = 0.
+Proof.
+elim: t=>[w b|_ l IHl r IHr] /=; rewrite !inE.
+- by move/negbTE=>->.
+by rewrite negb_or; case/andP=>/IHl->/IHr->.
+Qed.
+
+Lemma notin_alphabet_freqF_0 a ts :
+  a \notin alphabetF ts -> freqF ts a = 0.
+Proof.
+elim: ts=>//=t s IH; rewrite !inE negb_or.
+by case/andP=>/notin_alphabet_freq_0->/IH->.
+Qed.
+
+Lemma heightF_0_Leaf_freqF ts a :
+  consistentF ts -> heightF ts = 0 -> a \in alphabetF ts ->
+  Leaf (freqF ts a) a \in ts.
+Proof.
+elim: ts=>//=t s IH; case/and3P=>Hi Hct Hcs.
+move/eqP; rewrite maxn_eq0; case/andP=>/heightE [w][x] Et /= Hs.
+rewrite Et /= in Hi *.
+rewrite !inE; case: eqP=>/= [Ea|_].
+- move/alpha_notF: Hi=>/=; rewrite -Ea.
+  move=>/(_ a); rewrite inE eq_refl=>/(_ erefl) Has _.
+  by rewrite notin_alphabet_freqF_0 // addn0 eq_refl.
+rewrite add0n=>Has; apply/orP; right; apply: IH=>//.
+by apply/eqP.
+Qed.
+
+Lemma freqF_insortTree (p : tree A) ts a :
+  freqF (insortTree p ts) a = freq p a + freqF ts a.
+Proof.
+elim: ts=>//=t s IH; case: ifP=>//= _.
+by rewrite IH addnCA.
+Qed.
+
+Fixpoint weight (t : tree A) : nat :=
+  match t with
+  | Leaf w _ => w
+  | Node _ l r => weight l + weight r
+  end.
+
+Lemma height_0_cachedWeight t:
+  height t = 0 -> cachedWeight t = weight t.
+Proof. by case: t=>//=n l r; rewrite addn1. Qed.
+
+Fixpoint cost (t : tree A) : nat :=
+  if t is Node _ l r
+    then weight l + cost l + weight r + cost r
+  else 0.
+
+(* optimality *)
+
+Definition optimum (t : tree A) : Prop :=
+  forall u, consistent u ->
+            alphabet t =i alphabet u ->
+            freq t =1 freq u ->
+            cost t <= cost u.
+
+(* siblings *)
+
+(* weird that equations can't see t is decreasing *)
+Equations? sibling (t : tree A) (a : A) : A by wf (height t) lt :=
+sibling (Leaf _ _) a => a;
+sibling (Node _ (Leaf _ b) (Leaf _ c)) a =>
+  if a == b then c else if a == c then b else a;
+sibling (Node _ l r) a =>
+  if a \in alphabet l then sibling l a
+    else if a \in alphabet r then sibling r a
+      else a.
+Proof.
+all: apply: ssrnat.ltP.
+- by rewrite addn1.
+- by rewrite ltn_add2r max0n addn1.
+- by rewrite ltn_add2r leq_max addn1 ltnS leqnn.
+by rewrite addn1 ltnS leq_max leqnn orbT.
+Qed.
+
+Lemma in_alphabet_sibling t a:
+  a \in alphabet t -> sibling t a \in alphabet t.
+Proof.
+funelim (sibling t a)=>//; simp sibling=>/=; rewrite !inE.
+- case/orP=>->; first by rewrite eq_refl orbT.
+  by case: ifP=>_; rewrite eq_refl // orbT.
+- case/or3P=>E; rewrite !E //= ?orbT.
+  - case: ifP; first by move=>->.
+    move=>_; apply/orP; right.
+    by move: H0=>/=; rewrite !inE; apply; rewrite E.
+  case: ifP; first by move=>->.
+  move=>_; apply/orP; right.
+  by move: H0=>/=; rewrite !inE; apply; rewrite E orbT.
+rewrite -orbA; case/or3P=>E; rewrite E /= ?orbT.
+- apply/orP; left.
+  by move: H=>/=; rewrite !inE; apply; rewrite E.
+- apply/orP; left.
+  by move: H=>/=; rewrite !inE; apply; rewrite E orbT.
+case: ifP.
+- move=>Hlr; apply/orP; left.
+  by move: H=>/=; rewrite !inE; apply.
+by move=>_; rewrite (H0 E) orbT.
+Qed.
+
+Lemma notin_alphabet_sibling_id a t :
+  a \notin alphabet t -> sibling t a = a.
+Proof.
+funelim (sibling t a)=>//; simp sibling=>/=; rewrite !inE !negb_or -?andbA.
+- by case/andP=>/negbTE->/negbTE->.
+- by case/and3P=>/negbTE->/negbTE->/negbTE->.
+by case/and3P=>/negbTE->/negbTE->/negbTE->.
+Qed.
+
+Corollary sibling_ne_in_alphabet t a :
+  sibling t a != a -> sibling t a \in alphabet t.
+Proof.
+move=>H; apply: in_alphabet_sibling; move: H.
+by apply: contraR=>H; apply/eqP/notin_alphabet_sibling_id.
+Qed.
+
+Lemma height_gt0_sibling w p q a :
+  (0 < height p) || (0 < height q) ->
+  sibling (Node w p q) a =
+    if a \in alphabet p then sibling p a else sibling q a.
+Proof.
+case: q=>[wq q|wq ql qr]; case: p=>[wp p|wp pl pr]; simp sibling=>/=.
+- by rewrite ltnn.
+- by move=>_; rewrite !inE if_same.
+- move=>_; rewrite !inE; case: ifP=>//_; case: ifP=>//.
+  by move/negbT=>H; rewrite notin_alphabet_sibling_id.
+move=>_; rewrite !inE; case: ifP=>//_; case: ifP=>//.
+by move/negbT=>H; rewrite notin_alphabet_sibling_id.
+Qed.
+
+Lemma sibling_consistent_ind (P : tree A -> A -> Prop) t a :
+  consistent t ->
+  (forall w b a, P (Leaf w b) a) ->
+  (forall w wb b wc c a,
+     b != c -> P (Node w (Leaf wb b) (Leaf wc c)) a) ->
+  (forall w l r a,
+     consistent l -> consistent r ->
+     ~~ alpha_intersects l r ->
+     (0 < height l) || (0 < height r) ->
+     a \in alphabet l -> sibling l a \in alphabet l ->
+     a \notin alphabet r -> sibling l a \notin alphabet r ->
+     P l a ->
+     P (Node w l r) a) ->
+  (forall w l r a,
+     consistent l -> consistent r ->
+     ~~ alpha_intersects l r ->
+     (0 < height l) || (0 < height r) ->
+     a \notin alphabet l -> sibling r a \notin alphabet l ->
+     a \in alphabet r -> sibling r a \in alphabet r ->
+     P r a ->
+     P (Node w l r) a) ->
+  (forall w l r a,
+     consistent l -> consistent r ->
+     ~~ alpha_intersects l r ->
+     (0 < height l) || (0 < height r) ->
+     a \notin alphabet l -> a \notin alphabet r ->
+     P (Node w l r) a) ->
+  P t a.
+Proof.
+move=>Hc H0 Hn Hl Hr Hb; elim: t Hc=>[w b|w l IHl r IHr] /=.
+- by move=>_; apply: H0.
+case/and3P=>Hi Hcl Hcr.
+case: (posnP (height l + height r)).
+- move/eqP; rewrite addn_eq0; case/andP.
+  case/heightE=>[wb][b] El; case/heightE=>[wc][c] Er.
+  move: Hi; rewrite El Er /alpha_intersects /= orbF eq_sym.
+  by apply: Hn.
+rewrite addn_gt0=>Hh.
+case: (not_intersects a Hi); case=>Hil Hir.
+- have Hsl : sibling l a \in alphabet l by apply: in_alphabet_sibling.
+  by apply: Hl=>//; [move/alpha_not: Hi; apply |apply: IHl].
+- have Hsr : sibling r a \in alphabet r by apply: in_alphabet_sibling.
+  apply: Hr=>//; last by apply: IHr.
+  by move: Hi; rewrite intersectsC=>/alpha_not; apply.
+by apply: Hb.
+Qed.
+
+Lemma sibling_sibling_id t a :
+  consistent t -> sibling t (sibling t a) = a.
+Proof.
+move=>H.
+apply: (sibling_consistent_ind (P:=fun t a => sibling t (sibling t a) = a))=>{a}//=.
+- move=>w wb b wc c a /negbTE Hbc; simp sibling.
+  case/boolP: (a==b)=>[/eqP->|/negbTE Hab]; first by rewrite eq_sym Hbc eq_refl.
+  case/boolP: (a==c)=>[/eqP->|/negbTE Hac]; first by rewrite eq_refl.
+  by rewrite Hab Hac.
+- move=>w l r a _ _ _ Hh Hal Hsal _ _ IH.
+  by rewrite height_gt0_sibling // height_gt0_sibling // Hal Hsal.
+- move=>w l r a _ _ _ Hh /negbTE Hal /negbTE Hsal Har Hsar IH.
+  by rewrite height_gt0_sibling // height_gt0_sibling // Hal Hsal.
+move=>w l r a _ _ _ Hh Hal Har.
+by rewrite !notin_alphabet_sibling_id //= !inE negb_or Hal Har.
+Qed.
+
+Corollary sibling_reciprocal t a b :
+  consistent t -> sibling t a = b -> sibling t b = a.
+Proof. by move=>H <-; apply: sibling_sibling_id. Qed.
+
+Lemma depth_height_sibling_ne t a :
+  consistent t -> depth t a = height t -> 0 < height t ->
+  a \in alphabet t ->
+  sibling t a != a.
+Proof.
+move=>H.
+apply: (sibling_consistent_ind (P:=fun t a => depth t a = height t -> 0 < height t -> a \in alphabet t -> sibling t a != a))=>{a}//=.
+- move=>w wb b wc c a Hbc.
+  rewrite !inE maxn0 add0n; simp sibling; case: ifP=>/=.
+  - by move/eqP=>-> _ _ _; rewrite eq_sym.
+  by move=>_; case: ifP=>// /eqP->.
+- move=>w l r a _ _ _ Hh Hal _ _ _.
+  rewrite height_gt0_sibling // Hal =>IH /eqP; rewrite eqn_add2r=>E _ _.
+  apply: IH=>//.
+  - case: (leqP (height r) (height l)) E; first by move=>_/eqP.
+    by move=>Hlr /eqP Hd; move: (depth_le_height l a); rewrite Hd leqNgt Hlr.
+  case: (posnP (height l))=>// El; rewrite El ltnn /= in Hh.
+  case/eqP/heightE: El=>[wl][xl]El; rewrite El /= max0n eq_sym in E.
+  by move: Hh; move/eqP: E=>->.
+- move=>w l r a _ _ _ Hh /negbTE Hal _ Har _.
+  rewrite height_gt0_sibling // Hal Har =>IH /eqP; rewrite eqn_add2r=>E _ _.
+  apply: IH=>//.
+  - case: (leqP (height l) (height r)) E; first by move=>_/eqP.
+    by move=>Hrl /eqP Hd; move: (depth_le_height r a); rewrite Hd leqNgt Hrl.
+  case: (posnP (height r))=>// Er; rewrite Er ltnn /= orbF in Hh.
+  case/eqP/heightE: Er=>[wr][xr]Er; rewrite Er /= maxn0 eq_sym in E.
+  by move: Hh; move/eqP: E=>->.
+by move=>w l r a _ _ _ _ /negbTE Hal /negbTE Har _ _; rewrite !inE Hal Har.
+Qed.
+
+Lemma depth_sibling t a :
+  consistent t -> depth t (sibling t a) = depth t a.
+Proof.
+move=>H.
+apply: (sibling_consistent_ind (P:=fun t a => depth t (sibling t a) = depth t a))=>{a}//=.
+- move=>w wb b wc c a /negbTE Hbc; simp sibling; rewrite !inE.
+  case/boolP: (a==b)=>[_|/negbTE Hab].
+  - by rewrite eq_sym Hbc eq_refl.
+  case/boolP: (a==c); first by rewrite eq_refl.
+  by rewrite Hab =>/negbTE->.
+- move=>w l r a _ _ _ Hh Hal Hsal _ _ IH.
+  by rewrite height_gt0_sibling // Hal Hsal IH.
+- move=>w l r a _ _ _ Hh /negbTE Hal /negbTE Hsal Har Hsar IH.
+  by rewrite height_gt0_sibling // Hal Hsal Har Hsar IH.
+move=>w l r a _ _ _ Hh Hal Har.
+rewrite notin_alphabet_sibling_id; last by rewrite /= !inE negb_or Hal Har.
+by rewrite (negbTE Hal) (negbTE Har).
+Qed.
+
+End BasicAuxiliaryFunctions.
+
+Arguments consistent_ind [A P].
+
+Section OtherFunctions.
+Context {A : eqType}.
+
+(* swapping *)
+
+Fixpoint swapLeaves (t : tree A) (wa : nat) (a : A) (wb : nat) (b : A) : tree A :=
+  match t with
+  | Leaf wc c =>
+      if c == a then Leaf wb b else
+        if c == b then Leaf wa a else
+          Leaf wc c
+  | Node w l r =>
+      Node w (swapLeaves l wa a wb b) (swapLeaves r wa a wb b)
+  end.
+
+Lemma swapLeaves_id_notin_alphabet t w v a :
+  a \notin alphabet t -> swapLeaves t w a v a = t.
+Proof.
+elim: t=>[n b|n l IHl r IHr] /=; rewrite !inE.
+- by rewrite eq_sym=>/negbTE->.
+by rewrite negb_or; case/andP=>/IHl->/IHr->.
+Qed.
+
+Lemma swapLeaves_id t a :
+  consistent t -> swapLeaves t (freq t a) a (freq t a) a = t.
+Proof.
+(* TODO make nicer? *)
+move=>H.
+apply: (consistent_ind (P:=fun t a => swapLeaves t (freq t a) a (freq t a) a = t))=>{a}//=.
+- by move=>w b a; case: eqP=>//->; rewrite eq_refl.
+- move=>w l r a Hcl Hcr Hi Hal Har IHl IHr.
+  by rewrite (notin_alphabet_freq_0 Har) addn0 IHl swapLeaves_id_notin_alphabet.
+- move=>w l r a Hcl Hcr Hi Hal Har IHl IHr.
+  by rewrite (notin_alphabet_freq_0 Hal) add0n IHr swapLeaves_id_notin_alphabet.
+move=>w l r a Hcl Hcr Hi Hal Har IHl IHr.
+by rewrite (notin_alphabet_freq_0 Hal) (notin_alphabet_freq_0 Har) addn0
+  swapLeaves_id_notin_alphabet // swapLeaves_id_notin_alphabet.
+Qed.
+
+Lemma alphabet_swapLeaves t wa a wb b :
+  alphabet (swapLeaves t wa a wb b) =i
+    if a \in alphabet t then
+      if b \in alphabet t
+        then alphabet t
+        else [predU1 b & [predD1 (alphabet t) & a]]
+    else
+      if b \in alphabet t
+        then [predU1 a & [predD1 (alphabet t) & b]]
+        else SimplPred (alphabet t).
+Proof.
+move=>x; elim: t=>/=[w c|w l IHl r IHr]; rewrite !inE.
+- case: ifP.
+  - move/eqP=><-; rewrite eq_refl /= inE.
+    case: ifP; first by move/eqP=>->.
+    by move=>_; rewrite !inE andNb orbF.
+  rewrite eq_sym=>->; case: ifP.
+  - by move/eqP=>->; rewrite eq_refl /= !inE andNb orbF.
+  by rewrite eq_sym=>->/=; rewrite inE.
+rewrite {}IHl {}IHr.
+case/boolP: (a \in alphabet l)=>Hal; case/boolP: (a \in alphabet r)=>Har;
+case/boolP: (b \in alphabet l)=>Hbl; case/boolP: (b \in alphabet r)=>Hbr;
+rewrite /= !inE //;
+case: eqP=>[->|_]; case: eqP=>[->|_] //=;
+rewrite ?orbT ?orbF ?Hal ?Hbl ?Har ?Hbr ?orbT //.
+- by move/negbTE: Har; rewrite -topredE.
+- by move/negbTE: Hal; rewrite -topredE.
+- by move/negbTE: Hbr; rewrite -topredE.
+by move/negbTE: Hbl; rewrite -topredE.
+Qed.
+
+Lemma consistent_swapLeaves t wa a wb b :
+  consistent t -> consistent (swapLeaves t wa a wb b).
+Proof.
+elim: t=>[w c|w l IHl r IHr]/=.
+- by move=>_; case: ifP=>//_; case: ifP.
+case/and3P=>Hi Hl Hr; rewrite IHl // IHr //= andbT.
+apply/alpha_not=>z; rewrite !alphabet_swapLeaves.
+case: (not_intersects a Hi)=>[[        Hail /negbTE Hair]
+                             |[/negbTE Hail         Hair]
+                             |[/negbTE Hail /negbTE Hair]];
+case: (not_intersects b Hi)=>[[        Hbil /negbTE Hbir]
+                             |[/negbTE Hbil         Hbir]
+                             |[/negbTE Hbil /negbTE Hbir]];
+rewrite Hail Hair Hbil Hbir ?inE //.
+- by move/alpha_not: Hi; apply.
+- case: eqP=>[->|_] /=; rewrite negb_or.
+  - by rewrite andbT=>_; apply/eqP=>Hba; rewrite Hba Hail in Hbil.
+  by case: eqP=>//=_; move/alpha_not: (Hi); apply.
+- case: eqP=>[->|_] /=; first by move=>_; move: Hbir; rewrite -topredE /= =>->.
+  by case/andP=>_; move/alpha_not: (Hi); apply.
+- case: eqP=>[->|_] /=; rewrite negb_or.
+  - by rewrite andbT=>_; apply/eqP=>Hab; rewrite Hab Hbil in Hail.
+  by case: eqP=>//=_; move/alpha_not: (Hi); apply.
+- by move/alpha_not: Hi; apply.
+- rewrite negb_or; case: eqP=>[->|_] /=.
+  - by move: Hbil; rewrite -topredE /= =>->.
+  by case: eqP=>[->|_] //=; move/alpha_not: Hi; apply.
+- case: eqP=>[->|_] /=; first by move=>_; move: Hair; rewrite -topredE /= =>->.
+  by case: eqP=>//=_; move/alpha_not: (Hi); apply.
+- rewrite negb_or; case: eqP=>[->|_] /=.
+  - by move: Hail=>/[swap]; rewrite -topredE /= =>->.
+  by case: eqP=>[->|_] //=; move/alpha_not: Hi; apply.
+by move/alpha_not: Hi; apply.
+Qed.
+
+Lemma depth_swapLeaves t wa a wb b c :
+  consistent t -> c != a -> c != b ->
+  depth (swapLeaves t wa a wb b) c = depth t c.
+Proof.
+move=>H.
+apply: (consistent_ind (P:=fun t c => c != a -> c != b -> depth (swapLeaves t wa a wb b) c = depth t c))=>{c}//=.
+- by move=>w d c _ _; case: ifP=>//=_; case: ifP.
+- move=>_ l r c _ _ Hi Hcl _ IHl IHr Hca Hcb.
+  rewrite !alphabet_swapLeaves Hcl IHl // IHr //.
+  case: (not_intersects a Hi)=>[[        Hail /negbTE Hair]
+                               |[/negbTE Hail         Hair]
+                               |[/negbTE Hail /negbTE Hair]];
+  case: (not_intersects b Hi)=>[[        Hbil /negbTE Hbir]
+                               |[/negbTE Hbil         Hbir]
+                               |[/negbTE Hbil /negbTE Hbir]];
+  rewrite Hail Hair Hbil Hbir ?inE ?Hcl ?Hca ?Hcb /= ?orbT //.
+  - by move: Hcl; rewrite -topredE /==>->.
+  - by move: Hcl; rewrite -topredE /==>->.
+  - by move: Hcl; rewrite -topredE /==>->.
+  by move: Hcl; rewrite -topredE /==>->.
+- move=>_ l r c _ _ Hi /negbTE Hcl Hcr IHl IHr Hca Hcb.
+  rewrite !alphabet_swapLeaves Hcl Hcr IHl // IHr //.
+  case: (not_intersects a Hi)=>[[        Hail /negbTE Hair]
+                               |[/negbTE Hail         Hair]
+                               |[/negbTE Hail /negbTE Hair]];
+  case: (not_intersects b Hi)=>[[        Hbil /negbTE Hbir]
+                               |[/negbTE Hbil         Hbir]
+                               |[/negbTE Hbil /negbTE Hbir]];
+  rewrite Hail Hair Hbil Hbir ?inE ?Hcl ?Hcr ?Hca ?Hcb /= ?orbT ?andbF ?andbT ?orbF.
+  - by move: Hcr; rewrite -topredE /==>->.
+  - by rewrite (negbTE Hcb).
+  - by rewrite (negbTE Hcb); move: Hcr; rewrite -topredE /==>->.
+  - by rewrite (negbTE Hca).
+  - by move: Hcl; rewrite -topredE /==>->.
+  - by move: Hcl; rewrite -topredE /==>->.
+  - by rewrite (negbTE Hca); move: Hcr; rewrite -topredE /==>->.
+  - by move: Hcl; rewrite -topredE /==>->.
+  by move: Hcl Hcr; rewrite -!topredE /==>->->.
+move=>_ l r c _ _ Hi /negbTE Hcl /negbTE Hcr IHl IHr Hca Hcb.
+rewrite !alphabet_swapLeaves Hcl Hcr IHl // IHr //.
+case: (not_intersects a Hi)=>[[        Hail /negbTE Hair]
+                             |[/negbTE Hail         Hair]
+                             |[/negbTE Hail /negbTE Hair]];
+case: (not_intersects b Hi)=>[[        Hbil /negbTE Hbir]
+                             |[/negbTE Hbil         Hbir]
+                             |[/negbTE Hbil /negbTE Hbir]];
+rewrite Hail Hair Hbil Hbir ?inE ?Hcl ?Hcr ?Hca ?Hcb /= ?andbF ?andbT ?orbF.
+- by move: Hcr; rewrite -topredE /==>->.
+- by rewrite (negbTE Hcb) (negbTE Hca).
+- by rewrite (negbTE Hcb); move: Hcr; rewrite -topredE /==>->.
+- by rewrite (negbTE Hca) (negbTE Hcb).
+- by move: Hcl; rewrite -topredE /==>->.
+- by move: Hcl; rewrite (negbTE Hcb) -topredE /==>->.
+- by rewrite (negbTE Hca); move: Hcr; rewrite -topredE /==>->.
+- by move: Hcl; rewrite (negbTE Hca) -topredE /==>->.
+by move: Hcl Hcr; rewrite -!topredE /==>->->.
+Qed.
+
+Lemma height_swapLeaves t wa a wb b :
+  height (swapLeaves t wa a wb b) = height t.
+Proof.
+elim: t=>/=[w c|_ l IHl r IHr]; first by case: ifP=>//_; case: ifP.
+by rewrite IHl IHr.
+Qed.
+
+Lemma freq_swapLeaves t a b wa wb c :
+  consistent t -> a != b ->
+  freq (swapLeaves t wa a wb b) c =
+    if c == a
+      then if b \in alphabet t then wa else 0
+      else if c == b then
+        if a \in alphabet t then wb else 0
+        else freq t c.
+Proof.
+elim: t=>/=[w d|_ l IHl r IHr].
+- rewrite eq_sym=>_ Hba; rewrite !inE; case: eqP=>[->|/eqP Hda] /=.
+  - rewrite eq_refl (negbTE Hba).
+    case: eqP=>[->|_]; first by rewrite (negbTE Hba).
+    by case: ifP=>//->.
+  case: eqP=>[->|/eqP Hdb] /=.
+  - rewrite eq_refl (eq_sym a b) (negbTE Hba).
+    by case: eqP=>//_; case: ifP=>//->.
+  move: (Hda); rewrite eq_sym=>/negbTE->.
+  move: (Hdb); rewrite eq_sym=>/negbTE->.
+  case: eqP=>[->|_]; first by rewrite (negbTE Hda) (negbTE Hdb).
+  by rewrite !if_same.
+case/and3P=>Hi Hl Hr Hab. rewrite IHl // IHr // !inE.
+case: ifP=>_.
+- case: (not_intersects b Hi); case=>Hil Hir.
+  - by rewrite Hil (negbTE Hir) /= addn0.
+  - by rewrite (negbTE Hil) Hir /= add0n.
+  by rewrite (negbTE Hil) (negbTE Hir).
+case: ifP=>_ //.
+case: (not_intersects a Hi); case=>Hil Hir.
+- by rewrite Hil (negbTE Hir) /= addn0.
+- by rewrite (negbTE Hil) Hir /= add0n.
+by rewrite (negbTE Hil) (negbTE Hir).
+Qed.
+
+Lemma weight_swapLeaves t a b wa wb :
+  consistent t -> a != b ->
+  if a \in alphabet t then
+    if b \in alphabet t then
+      weight (swapLeaves t wa a wb b) + freq t a + freq t b =
+        weight t + wa + wb
+    else
+      weight (swapLeaves t wa a wb b) + freq t a = weight t + wb
+  else
+    if b \in alphabet t then
+      weight (swapLeaves t wa a wb b) + freq t b = weight t + wa
+    else
+      weight (swapLeaves t wa a wb b) = weight t.
+Proof.
+move=>H; apply: (consistent_ind (P:=fun t a => a != b -> if a \in alphabet t then if _ then _ = _ else _ else _)) =>{a}//=.
+- move=>w c a Hab; rewrite !inE; case: eqP; case: eqP.
+  - by move=><- E; rewrite E eq_refl in Hab.
+  - by move=>/[swap]<-; rewrite eq_sym eq_refl addnC.
+  - by move=><-; rewrite eq_sym eq_refl=>/eqP/negbTE->; rewrite addnC.
+  move/eqP/negbTE; rewrite eq_sym=>->.
+  by move/eqP/negbTE; rewrite eq_sym=>->.
+- move=>_ l r a Hcl Hcr Hi Hal Har IHl IHr Hab; rewrite !inE.
+  move: (IHr Hab); move: (IHl Hab).
+  rewrite Hal (negbTE Har) (notin_alphabet_freq_0 Har) addn0 /=.
+  case: (not_intersects b Hi); case=>Hbl Hbr.
+  - rewrite Hbl (negbTE Hbr) (notin_alphabet_freq_0 Hbr) /= =>H0->.
+    by rewrite addn0 (ACl ((1*3*4)*2)%AC) /= H0 (ACl (1*4*2*3)%AC).
+  - rewrite (negbTE Hbl) (notin_alphabet_freq_0 Hbl) /= Hbr =>H0 H1.
+    by rewrite add0n (ACl ((1*3)*(2*4))%AC) /= H0 H1 addnA (ACl (1*3*4*2)%AC).
+  rewrite (negbTE Hbl) (negbTE Hbr) /= =>H0->.
+  by rewrite addnAC H0 addnAC.
+- move=>_ l r a Hcl Hcr Hi Hal Har IHl IHr Hab; rewrite !inE.
+  move: (IHr Hab); move: (IHl Hab).
+  rewrite (negbTE Hal) Har (notin_alphabet_freq_0 Hal) add0n /=.
+  case: (not_intersects b Hi); case=>Hbl Hbr.
+  - rewrite Hbl (negbTE Hbr) (notin_alphabet_freq_0 Hbr) /= =>H0 H1.
+    by rewrite addn0 (ACl ((1*4)*(2*3))%AC) /= H0 H1 addnA (ACl (1*3*2*4)%AC).
+  - rewrite (negbTE Hbl) Hbr (notin_alphabet_freq_0 Hbl) /= =>->H1.
+    by rewrite add0n (ACl (1*(2*3*4))%AC) /= H1 !addnA.
+  rewrite (negbTE Hbl) (negbTE Hbr) /= =>->H1.
+  by rewrite -addnA H1 addnA.
+move=>_ l r a Hcl Hcr Hi Hal Har IHl IHr Hab; rewrite !inE.
+move: (IHr Hab); move: (IHl Hab); rewrite (negbTE Hal) (negbTE Har) /=.
+case: (not_intersects b Hi); case=>Hbl Hbr.
+- rewrite Hbl (negbTE Hbr) (notin_alphabet_freq_0 Hbr) /= =>H0->.
+  by rewrite addn0 addnAC H0 addnAC.
+- rewrite (negbTE Hbl) Hbr (notin_alphabet_freq_0 Hbl) /= =>->H1.
+  by rewrite add0n -addnA H1 addnA.
+by rewrite (negbTE Hbl) (negbTE Hbr) /= =>->->.
+Qed.
+
+Lemma cost_swapLeaves t a b wa wb :
+  a != b -> consistent t ->
+  if a \in alphabet t then
+    if b \in alphabet t then
+      cost (swapLeaves t wa a wb b) + freq t a * depth t a + freq t b * depth t b =
+        cost t + wa * depth t b + wb * depth t a
+    else
+      cost (swapLeaves t wa a wb b) + freq t a * depth t a =
+        cost t + wb * depth t a
+  else
+    if b \in alphabet t then
+      cost (swapLeaves t wa a wb b) + freq t b * depth t b =
+        cost t + wa * depth t b
+    else
+      cost (swapLeaves t wa a wb b) = cost t.
+Proof.
+move=>Hab; elim: t=>/=[w c|w l IHl r IHr]; rewrite !inE.
+- move=>_; case: eqP; case: eqP.
+  - by move=><- E; rewrite E eq_refl in Hab.
+  - by move=>/[swap]<-; rewrite eq_sym eq_refl !muln0.
+  - by move=><-; rewrite eq_sym eq_refl=>/eqP/negbTE->; rewrite !muln0.
+  move/eqP/negbTE; rewrite eq_sym=>->.
+  by move/eqP/negbTE; rewrite eq_sym=>->.
+case/and3P=>Hi Hcl Hcr; move: (IHr Hcr)=>{IHr}; move: (IHl Hcl)=>{IHl}.
+move: (weight_swapLeaves wa wb Hcr Hab); move: (weight_swapLeaves wa wb Hcl Hab).
+case: (not_intersects a Hi); case=>Hal Har;
+case: (not_intersects b Hi); case=>Hbl Hbr.
+- rewrite Hal (negbTE Har) Hbl (negbTE Hbr)
+    (notin_alphabet_freq_0 Har)
+    (notin_alphabet_freq_0 Hbr) /==>Wl -> Cl ->.
+  by rewrite !addn0 !mulnDr !muln1 !addnA (ACl ((1*6*8)*3*(2*5*7)*4)%AC) /=
+    Wl Cl !addnA (ACl (1*5*4*8*6*2*7*3)%AC).
+- rewrite Hal (negbTE Har) (negbTE Hbl) Hbr
+    (notin_alphabet_freq_0 Har)
+    (notin_alphabet_freq_0 Hbl) /==>Wl Wr Cl Cr.
+  by rewrite addn0 add0n !mulnDr !muln1 !addnA (ACl ((1*6)*(3*8)*(2*5)*(4*7))%AC) /=
+    Wl Wr Cl Cr !addnA (ACl (1*5*3*7*8*4*6*2)%AC).
+- rewrite Hal (negbTE Har) (negbTE Hbl) (negbTE Hbr)
+    (notin_alphabet_freq_0 Har)
+    (notin_alphabet_freq_0 Hbl) (notin_alphabet_freq_0 Hbr) /==>Wl -> Cl ->.
+  by rewrite addn0 !mulnDr !muln1 !addnA (ACl ((1*6)*(2*5)*3*4)%AC) /=
+    Wl Cl !addnA (ACl (1*3*5*6*4*2)%AC).
+- rewrite (negbTE Hal) Har Hbl (negbTE Hbr)
+    (notin_alphabet_freq_0 Hal)
+    (notin_alphabet_freq_0 Hbr) /==>Wl Wr Cl Cr.
+  by rewrite addn0 add0n !mulnDr !muln1 !addnA (ACl ((1*8)*(3*6)*(2*7)*(4*5))%AC) /=
+    Wl Wr Cl Cr !addnA (ACl (1*5*3*7*6*2*8*4)%AC).
+- rewrite (negbTE Hal) Har (negbTE Hbl) Hbr
+    (notin_alphabet_freq_0 Hal)
+    (notin_alphabet_freq_0 Hbl) /==>-> Wr -> Cr.
+  by rewrite !add0n !mulnDr !muln1 !addnA (ACl (1*2*(3*6*8)*(4*5*7))%AC) /=
+    Wr Cr !addnA (ACl (1*2*3*6*7*4*8*5)%AC).
+- rewrite (negbTE Hal) Har (negbTE Hbl) (negbTE Hbr)
+    (notin_alphabet_freq_0 Hal)
+    (notin_alphabet_freq_0 Hbl) (notin_alphabet_freq_0 Hbr) /==>-> Wr -> Cr.
+  by rewrite add0n !mulnDr !muln1 !addnA (ACl (1*2*(3*6)*(4*5))%AC) /=
+    Wr Cr !addnA (ACl (1*2*3*5*6*4)%AC).
+- rewrite (negbTE Hal) (negbTE Har) Hbl (negbTE Hbr)
+    (notin_alphabet_freq_0 Hal) (notin_alphabet_freq_0 Har)
+    (notin_alphabet_freq_0 Hbr) /==>Wl -> Cl ->.
+  by rewrite addn0 !mulnDr !muln1 !addnA (ACl ((1*6)*(2*5)*3*4)%AC) /=
+    Wl Cl !addnA (ACl (1*3*5*6*4*2)%AC).
+- rewrite (negbTE Hal) (negbTE Har) (negbTE Hbl) Hbr
+    (notin_alphabet_freq_0 Hal) (notin_alphabet_freq_0 Har)
+    (notin_alphabet_freq_0 Hbl) /==>-> Wr -> Cr.
+  by rewrite add0n !mulnDr !muln1 !addnA (ACl (1*2*(3*6)*(4*5))%AC) /=
+    Wr Cr !addnA (ACl (1*2*3*5*6*4)%AC).
+by rewrite (negbTE Hal) (negbTE Har) (negbTE Hbl) (negbTE Hbr)
+    (notin_alphabet_freq_0 Hal) (notin_alphabet_freq_0 Har)
+    (notin_alphabet_freq_0 Hbl) (notin_alphabet_freq_0 Hbr) /==>->->->->.
+Qed.
+
+Lemma sibling_swapLeaves_sibling t wa a ws b :
+  consistent t -> sibling t b != b -> a != b ->
+  sibling (swapLeaves t wa a ws (sibling t b)) a = b.
+Proof.
+elim: t=>/=[w c|w l IHl r IHr].
+- by move=>_; simp sibling; rewrite eq_refl.
+case: (posnP (height l))=>El; case: (posnP (height r))=>Er.
+- case/eqP/heightE: El=>[wl][xl]->; case/eqP/heightE: Er=>[wr][xr]-> /=.
+  simp sibling; rewrite /alpha_intersects /= orbF andbT =>/negbTE Hrl; case: ifP=>[/eqP->|Hbxl].
+  - move=>_; rewrite eq_sym=>/negbTE Haxl.
+    rewrite Haxl eq_sym Hrl eq_refl; case: ifP; simp sibling.
+    - by rewrite eq_sym=>->; rewrite eq_sym Haxl.
+    by move=>_; rewrite eq_sym Haxl eq_refl.
+  case: ifP; last by rewrite eq_refl.
+  move/eqP=>-> _; rewrite eq_sym=>/negbTE Haxr; rewrite eq_refl Hrl Haxr.
+  case: ifP; simp sibling; first by rewrite eq_sym=>->.
+  by rewrite eq_refl.
+- rewrite height_gt0_sibling; last by rewrite Er orbT.
+  case/eqP/heightE: El=>[wl][xl]->/=; rewrite /alpha_intersects /= inE; simp sibling.
+  case/andP=>Hxlr Hcr; case: ifP; first by rewrite eq_refl.
+  move=>Hbxl Hsrb Hab.
+  have Hsab : sibling r b \in alphabet r by apply: sibling_ne_in_alphabet.
+  have Hxsb : sibling r b != xl.
+  - by rewrite alphabet_enum in Hsab; move/hasPn: Hxlr=>/(_ _ Hsab).
+  rewrite height_gt0_sibling; last by rewrite height_swapLeaves Er orbT.
+  case/boolP: (xl==a)=>/=.
+  - rewrite inE; move/eqP=>{1}<-; rewrite eq_sym (negbTE Hxsb).
+    by apply: IHr.
+  move=>Haxl; rewrite eq_sym (negbTE Hxsb) /= inE eq_sym (negbTE Haxl).
+  by apply: IHr.
+- rewrite height_gt0_sibling; last by rewrite El.
+  case/eqP/heightE: Er=>[wr][xr]->/=; rewrite /alpha_intersects /= orbF andbT; simp sibling.
+  case/andP=>Hlxr Hcl; case: ifP; last by rewrite eq_refl.
+  move=>Hbal Hslb Hab.
+  have Hsab : sibling l b \in alphabet l by apply: sibling_ne_in_alphabet.
+  rewrite height_gt0_sibling; last by rewrite height_swapLeaves El.
+  rewrite alphabet_swapLeaves Hsab; case/boolP: (a \in alphabet l)=>/=.
+  - by move=>->; apply: IHl.
+  by move=>_; rewrite !inE eq_refl /=; apply: IHl.
+case/and3P=>Hi Hcl Hcr.
+rewrite height_gt0_sibling; last by rewrite El.
+case/boolP: (b \in alphabet l)=>Hbal Hsb Hab.
+- have Hsab : sibling l b \in alphabet l by apply: sibling_ne_in_alphabet.
+  rewrite height_gt0_sibling; last by rewrite height_swapLeaves El.
+  rewrite alphabet_swapLeaves Hsab; case/boolP: (a \in alphabet l)=>/=.
+  - by move=>->; apply: IHl.
+  by move=>_; rewrite !inE eq_refl /=; apply: IHl.
+rewrite height_gt0_sibling; last by rewrite height_swapLeaves El.
+have Hsab : sibling r b \in alphabet r by apply: sibling_ne_in_alphabet.
+move: Hi; rewrite intersectsC=>/alpha_not/(_ _ Hsab)=>Hsab'.
+rewrite alphabet_swapLeaves (negbTE Hsab'); case/boolP: (a \in alphabet l)=>/=.
+- move=>Hal; rewrite !inE eq_refl /= orbF; case: eqP=>[E|_]; last by apply IHr.
+  by rewrite -E Hal in Hsab'.
+by rewrite inE=>/negbTE->; apply: IHr.
+Qed.
+
+Definition swapSyms (t : tree A) (a b : A) : tree A :=
+  swapLeaves t (freq t a) a (freq t b) b.
+
+Corollary swapSyms_id t a :
+  consistent t -> swapSyms t a a = t.
+Proof. by move=>H; apply: swapLeaves_id. Qed.
+
+Lemma alphabet_swapSyms t a b :
+  a \in alphabet t -> b \in alphabet t -> alphabet (swapSyms t a b) =i alphabet t.
+Proof.
+move=>Ha Hb; rewrite /swapSyms=>x.
+by rewrite alphabet_swapLeaves Ha Hb.
+Qed.
+
+Lemma consistent_swapSyms t a b :
+  consistent t -> consistent (swapSyms t a b).
+Proof. by exact: consistent_swapLeaves. Qed.
+
+Lemma depth_swapSyms t c a b :
+  consistent t -> c != a -> c != b ->
+  depth (swapSyms t a b) c = depth t c.
+Proof. by exact: depth_swapLeaves. Qed.
+
+Lemma freq_swapSyms t a b :
+  consistent t -> a \in alphabet t -> b \in alphabet t ->
+  freq (swapSyms t a b) =1 freq t.
+Proof.
+move=>Hc Ha Hb; case/boolP: (a == b)=>[/eqP->|Hab] c.
+- by rewrite swapSyms_id.
+rewrite /swapSyms freq_swapLeaves // Ha Hb.
+by case: eqP=>[->|_] //; case: eqP=>[->|_].
+Qed.
+
+Lemma cost_swapSyms t a b :
+  consistent t -> a \in alphabet t -> b \in alphabet t ->
+  cost (swapSyms t a b) + freq t a * depth t a + freq t b * depth t b =
+                 cost t + freq t a * depth t b + freq t b * depth t a.
+Proof.
+case/boolP: (a == b).
+- by move/eqP=>->Hc Hb _; rewrite swapSyms_id.
+move=>Hab Hc Hat Hbt; rewrite /swapSyms.
+by move: (cost_swapLeaves (freq t a) (freq t b) Hab Hc); rewrite Hat Hbt.
+Qed.
+
+(* 13.1 *)
+Lemma cost_swapSyms_le t a b:
+  consistent t -> a \in alphabet t -> b \in alphabet t ->
+  freq t a <= freq t b -> depth t a <= depth t b ->
+  cost (swapSyms t a b) <= cost t.
+Proof.
+move=>Ht Ha Hb.
+set i := freq t a; set m := depth t a.
+set j := freq t b; set n := depth t b.
+move=>Hf Hd.
+set aabb := i * m + j * n.
+set abba := i * n + j * m.
+have H1: abba <= aabb.
+- rewrite /abba /aabb.
+  have : i * m + i * (n - m) + j * m <= i * m + j * m + j * (n - m).
+  - by rewrite -!addnA leq_add2l addnC leq_add2l leq_mul2r Hf orbT.
+  rewrite !mulnBr addnBCA //; last by rewrite leq_mul2l Hd orbT.
+  rewrite subnn addn0 -addnA addnBCA //; last by rewrite leq_mul2l Hd orbT.
+  by rewrite subnn addn0.
+have H2: cost (swapSyms t a b) + aabb = cost t + abba.
+- by rewrite /aabb /abba /i /m /j /n !addnA; apply: cost_swapSyms.
+rewrite -(leq_add2r aabb); apply: leq_trans; first by rewrite H2; apply: leqnn.
+by rewrite leq_add2l.
+Qed.
+
+Corollary sibling_swapSyms_sibling t a b :
+  consistent t -> sibling t b != b -> a != b ->
+  sibling (swapSyms t a (sibling t b)) a = b.
+Proof. by exact: sibling_swapLeaves_sibling. Qed.
+
+Lemma sibling_swapSyms_other_sibling t a b:
+  consistent t -> sibling t b != a -> sibling t b != b -> a != b ->
+  sibling (swapSyms t a b) (sibling t b) = a.
+Proof.
+move=>H Ha Hb Hab.
+apply: sibling_reciprocal; first by apply: consistent_swapSyms.
+rewrite -{1}(sibling_sibling_id (t:=t) b) // sibling_swapSyms_sibling // eq_sym //.
+by rewrite sibling_sibling_id.
+Qed.
+
+Definition swapFourSyms (t : tree A) (a b c d : A) : tree A :=
+  if a == d then swapSyms t b c
+    else if b == c then swapSyms t a d
+      else swapSyms (swapSyms t a c) b d.
+
+Lemma alphabet_swapFourSyms t a b c d :
+  a \in alphabet t -> b \in alphabet t -> c \in alphabet t -> d \in alphabet t ->
+  alphabet (swapFourSyms t a b c d) =i alphabet t.
+Proof.
+move=>Ha Hb Hc Hd; rewrite /swapFourSyms.
+case: ifP=>_; first by apply: alphabet_swapSyms.
+by case: ifP=>_ z; rewrite !alphabet_swapSyms.
+Qed.
+
+Lemma consistent_swapFourSyms t a b c d :
+  consistent t -> consistent (swapFourSyms t a b c d).
+Proof.
+move=>H; rewrite /swapFourSyms.
+case: ifP=>_; first by apply: consistent_swapSyms.
+by case: ifP=>_; rewrite !consistent_swapSyms.
+Qed.
+
+Lemma freq_swapFourSyms t a b c d :
+  consistent t ->
+  a \in alphabet t -> b \in alphabet t -> c \in alphabet t -> d \in alphabet t ->
+  freq (swapFourSyms t a b c d) =1 freq t.
+Proof.
+move=>H Ha Hb Hc Hd; rewrite /swapFourSyms.
+case: ifP=>_; first by apply: freq_swapSyms.
+case: ifP=>_; first by apply: freq_swapSyms.
+move=>z; rewrite !freq_swapSyms ?alphabet_swapSyms //.
+by apply: consistent_swapSyms.
+Qed.
+
+Lemma sibling_swapFourSyms t a b c :
+  consistent t ->
+  a != b -> sibling t c != c ->
+  sibling (swapFourSyms t a b c (sibling t c)) a = b.
+Proof.
+move=>H Hab Hs; case/boolP: ((a != sibling t c) && (b != c)).
+- set d := sibling t c in Hs *.
+  case/andP=>Had Hbc.
+  set s := swapFourSyms t a b c d.
+  have Hcs : consistent s by apply: consistent_swapFourSyms.
+  apply: sibling_reciprocal=>//.
+  have Ed : d = sibling (swapSyms t a c) a.
+  - symmetry; rewrite /d -{1}(sibling_sibling_id (t:=t) c) //.
+    apply: sibling_swapSyms_sibling=>//.
+    by rewrite eq_sym sibling_sibling_id.
+  rewrite /s /swapFourSyms (negbTE Had) (negbTE Hbc).
+  case/boolP: (a == c)=>[/eqP->|Hac].
+  - by rewrite swapSyms_id //; apply: sibling_swapSyms_sibling.
+  have {2}<-: sibling (swapSyms t a c) d = a.
+  - rewrite /d; apply: sibling_swapSyms_other_sibling=>//.
+    by rewrite eq_sym.
+  rewrite Ed sibling_sibling_id; last by apply: consistent_swapSyms.
+  apply: sibling_swapSyms_sibling.
+  - by apply: consistent_swapSyms.
+  - by rewrite -Ed eq_sym.
+  by rewrite eq_sym.
+rewrite /swapFourSyms negb_and.
+case/boolP: (a == sibling t c); case/boolP: (b == c)=>//=.
+- by move/eqP=>->/eqP Has _; rewrite swapSyms_id // Has sibling_sibling_id.
+- move=>Hbc /eqP Has _; rewrite Has; apply: sibling_swapSyms_other_sibling=>//.
+  by rewrite -Has.
+by move/eqP=>Hbc _ _; rewrite Hbc in Hab *; apply: sibling_swapSyms_sibling.
+Qed.
+
+(* merging *)
+
+Equations? mergeSibling (t : tree A) (a : A) : tree A by wf (height t) lt :=
+mergeSibling (Leaf wb b) a => Leaf wb b;
+mergeSibling (Node w (Leaf wb b) (Leaf wc c)) a =>
+  if (a == b) || (a == c)
+    then Leaf (wb + wc) a
+    else Node w (Leaf wb b) (Leaf wc c);
+mergeSibling (Node w l r) a =>
+  Node w (mergeSibling l a) (mergeSibling r a).
+Proof.
+all: apply: ssrnat.ltP.
+- by rewrite addn1.
+- by rewrite ltn_add2r max0n addn1.
+- by rewrite ltn_add2r leq_max addn1 ltnS leqnn.
+by rewrite addn1 ltnS leq_max leqnn orbT.
+Qed.
+
+Lemma notin_alphabet_mergeSibling_id a t :
+  a \notin alphabet t -> mergeSibling t a = t.
+Proof.
+funelim (mergeSibling t a)=>//; simp mergeSibling=>/=; rewrite !inE.
+- by move/negbTE=>->.
+- rewrite !negb_or; case/and3P=>Has Hal Har.
+  by rewrite H0 //= !inE negb_or Hal Har.
+rewrite !negb_or -andbA; case/and3P=>Hap Haq Har.
+rewrite H /=; first by rewrite H0.
+by rewrite !inE negb_or Hap Haq.
+Qed.
+
+Lemma height_gt0_mergeSibling w p q a :
+  (0 < height p) || (0 < height q) ->
+  mergeSibling (Node w p q) a =
+    Node w (mergeSibling p a) (mergeSibling q a).
+Proof. by case: q=>[wq q|wq ql qr]; case: p=>[wp p|wp pl pr]; simp mergeSibling. Qed.
+
+Lemma alphabet_mergeSibling t a :
+  consistent t -> a \in alphabet t ->
+  alphabet (mergeSibling t a) =i [predU1 a & [predD1 (alphabet t) & (sibling t a)]].
+Proof.
+move=>H; apply: (sibling_consistent_ind (P:=fun t a => a \in alphabet t -> alphabet (mergeSibling t a) =i [predU1 a & [predD1 (alphabet t) & (sibling t a)]])) =>{a}//=.
+- move=>w b a; rewrite inE=>/eqP->; simp sibling mergeSibling=>/= z.
+  by rewrite !inE; case: eqP.
+- move=>w wb b wc c a Hbc; rewrite !inE.
+  simp sibling mergeSibling; case/orP=>/eqP->; rewrite eq_refl ?orbT /= => z; rewrite !inE.
+  - by case: eqP=>//= _; rewrite andNb.
+  by case: eqP=>//= _; rewrite orbF (eq_sym c b) (negbTE Hbc) andNb.
+- move=>w l r a _ _ _ Hh Hal _ Har Hsar IH _.
+  rewrite height_gt0_mergeSibling //= height_gt0_sibling // Hal
+    (notin_alphabet_mergeSibling_id Har) => z.
+  by rewrite !inE IH // !inE; case: eqP=>//= _; case: eqP=>//= ->; apply/negbTE.
+- move=>w l r a _ _ _ Hh Hal Hsal Har _ IH _.
+  rewrite height_gt0_mergeSibling //= height_gt0_sibling // (negbTE Hal)
+    (notin_alphabet_mergeSibling_id Hal) => z.
+  rewrite !inE IH // !inE; case: eqP=>/= _; first by rewrite orbT.
+  by case: eqP=>//=->; rewrite orbF; apply/negbTE.
+by move=>w l r a _ _ _ _ Hal Har; rewrite !inE (negbTE Hal) (negbTE Har).
+Qed.
+
+Lemma consistent_mergeSibling t a :
+  consistent t -> consistent (mergeSibling t a).
+Proof.
+move=>H; apply: (sibling_consistent_ind (P:=fun t a => consistent (mergeSibling t a))) =>{a}//=.
+- move=>w wb b wc c a Hbc; simp mergeSibling; case: ifP=>//= _.
+  by rewrite andbT /alpha_intersects /= orbF eq_sym.
+- move=>w l r a Hcl Hcr Hi Hh Hal _ Har _ IH.
+  rewrite height_gt0_mergeSibling //= (notin_alphabet_mergeSibling_id Har) IH Hcr /= andbT.
+  apply/alpha_not=>z; rewrite alphabet_mergeSibling // !inE.
+  case: eqP=>[->|_] //=; case/andP=>_.
+  by move/alpha_not: Hi; apply.
+- move=>w l r a Hcl Hcr Hi Hh Hal _ Har _ IH.
+  rewrite height_gt0_mergeSibling //= (notin_alphabet_mergeSibling_id Hal) IH Hcl /= andbT.
+  rewrite intersectsC; apply/alpha_not=>z; rewrite alphabet_mergeSibling // !inE.
+  case: eqP=>[->|_] //=; case/andP=>_.
+  by move: Hi; rewrite intersectsC =>/alpha_not; apply.
+move=>w l r a Hcl Hcr Hi Hh Hal Har.
+by rewrite height_gt0_mergeSibling //=
+  (notin_alphabet_mergeSibling_id Hal) (notin_alphabet_mergeSibling_id Har) Hi Hcl Hcr.
+Qed.
+
+Lemma freq_mergeSibling t a z :
+  consistent t -> a \in alphabet t -> sibling t a != a ->
+  freq (mergeSibling t a) z =
+    if z == a then freq t a + freq t (sibling t a)
+      else if z == sibling t a
+             then 0
+             else freq t z.
+Proof.
+move=>H; apply: (sibling_consistent_ind (P:=fun t a => a \in alphabet t -> sibling t a != a -> freq (mergeSibling t a) z = if z == a then freq t a + freq t (sibling t a) else if z == sibling t a then 0 else freq t z)) =>{a}//=.
+- by move=>w b a _; simp sibling; rewrite eq_refl.
+- move=>w wb b wc c a Hbc; rewrite !inE.
+  simp sibling mergeSibling; case/orP=>/eqP->; rewrite eq_refl /=.
+  - move=>_; rewrite (negbTE Hbc) eq_refl (eq_sym c b) (negbTE Hbc) addn0 add0n.
+    by case: eqP=>// _; case: eqP.
+  rewrite (eq_sym c b) !(negbTE Hbc) /= eq_refl add0n addn0 => _.
+  case: eqP; first by rewrite addnC.
+  by case: eqP.
+- move=>w l r a _ _ _ Hh Hal _ Har Hsar IH _.
+  rewrite height_gt0_mergeSibling //= height_gt0_sibling // Hal
+    (notin_alphabet_mergeSibling_id Har)
+    (notin_alphabet_freq_0 Har) (notin_alphabet_freq_0 Hsar) !addn0 => Hsl.
+  rewrite IH //; case: eqP=>[->|_].
+  - by rewrite (notin_alphabet_freq_0 Har) addn0.
+  by case: eqP=>//->; rewrite (notin_alphabet_freq_0 Hsar).
+- move=>w l r a _ _ _ Hh Hal Hsal Har _ IH _.
+  rewrite height_gt0_mergeSibling //= height_gt0_sibling // (negbTE Hal)
+    (notin_alphabet_mergeSibling_id Hal)
+    (notin_alphabet_freq_0 Hal) (notin_alphabet_freq_0 Hsal) !add0n => Hsr.
+  rewrite IH //; case: eqP=>[->|_].
+  - by rewrite (notin_alphabet_freq_0 Hal) add0n.
+  by case: eqP=>//->; rewrite (notin_alphabet_freq_0 Hsal).
+by move=>w l r a _ _ _ _ Hal Har; rewrite !inE (negbTE Hal) (negbTE Har).
+Qed.
+
+Lemma weight_mergeSibling t a :
+  weight (mergeSibling t a) = weight t.
+Proof.
+funelim (mergeSibling t a)=>//; simp mergeSibling=>/=.
+- by case: ifP.
+- by rewrite H0.
+by rewrite H0 H.
+Qed.
+
+(* 13.2 *)
+Lemma cost_mergeSibling t a :
+  consistent t -> sibling t a != a ->
+  cost (mergeSibling t a) + freq t a + freq t (sibling t a) = cost t.
+Proof.
+move=>H; apply: (sibling_consistent_ind (P:=fun t a => sibling t a != a -> cost (mergeSibling t a) + freq t a + freq t (sibling t a) = cost t)) =>{a}//=.
+- by move=>w b a; simp sibling; rewrite eq_refl.
+- move=>w wb b wc c a Hbc; simp sibling mergeSibling=>/=; case: ifP=>/=.
+  - by move/eqP=>-> Hcb; rewrite eq_sym (negbTE Hcb) eq_refl !addn0 !add0n.
+  move/negbT=>Hab; case: ifP=>/=; last by rewrite eq_refl.
+  by move/eqP=>->_; rewrite eq_refl (negbTE Hbc) !addn0 !add0n addnC.
+- move=>w l r a _ _ _ Hh Hal _ Har Hslar IHl.
+  rewrite height_gt0_sibling // height_gt0_mergeSibling //= Hal
+    (notin_alphabet_mergeSibling_id Har) weight_mergeSibling
+    (notin_alphabet_freq_0 Har) (notin_alphabet_freq_0 Hslar) !addn0
+    (ACl (1*(2*5*6)*3*4)%AC) /=.
+  by move/IHl=>->.
+- move=>w l r a _ _ _ Hh Hal Hslal Har _ IHr.
+  rewrite height_gt0_sibling // height_gt0_mergeSibling //= (negbTE Hal)
+    (notin_alphabet_mergeSibling_id Hal) weight_mergeSibling
+    (notin_alphabet_freq_0 Hal) (notin_alphabet_freq_0 Hslal) !add0n
+    (ACl (1*2*3*(4*5*6))%AC) /=.
+  by move/IHr=>->.
+move=>w l r a _ _ _ Hh Hal Har Hn.
+rewrite notin_alphabet_sibling_id /=; last by rewrite !inE negb_or Hal Har.
+rewrite notin_alphabet_mergeSibling_id /=; last by rewrite !inE negb_or Hal Har.
+by rewrite !notin_alphabet_freq_0 // !addn0.
+Qed.
+
+(* splitting *)
+
+Fixpoint splitLeaf (t : tree A) (wa : nat) (a : A) (wb : nat) (b : A) : tree A :=
+  match t with
+  | Leaf wc c =>
+      if c == a then Node wc (Leaf wa a) (Leaf wb b)
+                else Leaf wc c
+  | Node w l r =>
+      Node w (splitLeaf l wa a wb b) (splitLeaf r wa a wb b)
+  end.
+
+Fixpoint splitLeafF (ts : forest A) (wa : nat) (a : A) (wb : nat) (b : A) : forest A :=
+  if ts is t::s
+    then splitLeaf t wa a wb b :: splitLeafF s wa a wb b
+    else [::].
+
+Lemma notin_alphabet_splitLeaf_id t a wa b wb :
+  a \notin alphabet t -> splitLeaf t wa a wb b = t.
+Proof.
+elim: t=>/=[w c|w l IHl r IHr]; rewrite !inE.
+- by rewrite eq_sym=>/negbTE->.
+by rewrite negb_or; case/andP=>/IHl->/IHr->.
+Qed.
+
+Lemma notin_alphabet_splitLeafF_id ts wa a wb b :
+  a \notin alphabetF ts -> splitLeafF ts wa a wb b = ts.
+Proof.
+elim: ts=>//=q s IH; rewrite !inE negb_or; case/andP=>Hq Hs.
+by rewrite notin_alphabet_splitLeaf_id // IH.
+Qed.
+
+Lemma cachedWeight_splitLeaf (t : tree A) wa a wb b :
+  cachedWeight (splitLeaf t wa a wb b) = cachedWeight t.
+Proof. by case: t=>//=n c; case: ifP. Qed.
+
+Lemma alphabet_splitLeaf t wa a wb b :
+  alphabet (splitLeaf t wa a wb b) =i
+    if a \in alphabet t then [predU1 b & (alphabet t)] else SimplPred (alphabet t).
+Proof.
+elim: t=>/= [w c|_ l IHl r IHr] z; rewrite !inE.
+- case: ifP; last by rewrite eq_sym=>->/=.
+  by move/eqP=>->; rewrite eq_refl !inE orbC.
+rewrite {}IHl {}IHr.
+case/boolP: (a \in alphabet l)=>Hl; case/boolP: (a \in alphabet r)=>Hr //=;
+rewrite !inE; case: eqP=>[->|_] //=.
+by rewrite orbT.
+Qed.
+
+Lemma consistent_splitLeaf t wa a wb b :
+  consistent t -> b \notin alphabet t ->
+  consistent (splitLeaf t wa a wb b).
+Proof.
+elim: t=>/=[w c|_ l IHl r IHr].
+- move=>_; rewrite inE=>Hbc; case: ifP=>//=.
+  by move/eqP=><-; rewrite andbT /alpha_intersects /= orbF.
+case/and3P=>Hi Hcl Hcr; rewrite !inE negb_or; case/andP=>Hbl Hbr.
+rewrite IHl // IHr //= andbT.
+apply/alpha_not=>z; rewrite !alphabet_splitLeaf.
+case: (not_intersects a Hi); case.
+- move=>->/negbTE->; rewrite !inE; case: eqP=>[->|_] /=.
+  - by move=>_; move: Hbr; rewrite -topredE /=.
+  by move/alpha_not: Hi; apply.
+- move=>/negbTE->->; rewrite !inE; case: eqP=>[->|_] /=.
+  - by move: Hbl; rewrite -topredE /==>/[swap]->.
+  by move/alpha_not: Hi; apply.
+move=>/negbTE->/negbTE->; rewrite !inE.
+by move/alpha_not: Hi; apply.
+Qed.
+
+Lemma freq_splitLeaf t wa a wb b z :
+  consistent t -> b \notin alphabet t ->
+  freq (splitLeaf t wa a wb b) z =
+    if a \in alphabet t then
+      if z == a then wa else if z == b then wb else freq t z
+    else freq t z.
+Proof.
+move=>H; apply: (consistent_ind (P:=fun t a => b \notin alphabet t -> freq (splitLeaf t wa a wb b) z = if a \in alphabet t then if z == a then wa else if z == b then wb else freq t z else freq t z))=>//={a}.
+- move=>w c a; rewrite !inE=>Hbc; case: ifP=>Hca /=.
+  - rewrite (eqP Hca) in Hbc *; rewrite eq_refl; case: ifP; last by rewrite add0n.
+    by move: Hbc=>/[swap]/eqP->; rewrite eq_sym=>/negbTE->; rewrite addn0.
+  by rewrite (eq_sym a c) Hca.
+- move=>_ l r a _ _ _ Hal Har IHl IHr; rewrite !inE negb_or; case/andP=>Hbl Hbr.
+  rewrite IHl // IHr // Hal (negbTE Har) /=; case: ifP.
+  - by move/eqP=>->; rewrite (notin_alphabet_freq_0 Har) addn0.
+  move=>_; case: ifP=>// /eqP->.
+  by rewrite (notin_alphabet_freq_0 Hbr) addn0.
+- move=>_ l r a _ _ _ Hal Har IHl IHr; rewrite !inE negb_or; case/andP=>Hbl Hbr.
+  rewrite IHl // IHr // (negbTE Hal) Har /=; case: ifP.
+  - by move/eqP=>->; rewrite (notin_alphabet_freq_0 Hal) add0n.
+  move=>_; case: ifP=>// /eqP->.
+  by rewrite (notin_alphabet_freq_0 Hbl) add0n.
+move=>_ l r a _ _ _ Hal Har IHl IHr; rewrite !inE negb_or; case/andP=>Hbl Hbr.
+by rewrite IHl // IHr // (negbTE Hal) (negbTE Har).
+Qed.
+
+Lemma weight_splitLeaf t a wa b wb :
+  consistent t -> a \in alphabet t -> freq t a = wa + wb ->
+  weight (splitLeaf t wa a wb b) = weight t.
+Proof.
+move=>H; apply: (consistent_ind (P:=fun t a => a \in alphabet t -> freq t a = wa + wb -> weight (splitLeaf t wa a wb b) = weight t))=>//={a}.
+- by move=>w c a; rewrite inE=>/eqP->; rewrite eq_refl /= =>->.
+- move=>_ l r a _ _ _ Hal Har IHl _ _.
+  rewrite (notin_alphabet_freq_0 Har) addn0=>Hf.
+  by rewrite (notin_alphabet_splitLeaf_id _ _ _ Har) IHl.
+- move=>_ l r a _ _ _ Hal Har _ IHr _.
+  rewrite (notin_alphabet_freq_0 Hal) add0n=>Hf.
+  by rewrite (notin_alphabet_splitLeaf_id _ _ _ Hal) IHr.
+by move=>_ l r a _ _ _ /negbTE Hal /negbTE Har _ _; rewrite !inE Hal Har.
+Qed.
+
+(* 13.3 *)
+Lemma cost_splitLeaf t a wa b wb :
+  consistent t -> a \in alphabet t -> freq t a = wa + wb ->
+  cost (splitLeaf t wa a wb b) = cost t + wa + wb.
+Proof.
+move=>H; apply: (consistent_ind (P:=fun t a => a \in alphabet t -> freq t a = wa + wb -> cost (splitLeaf t wa a wb b) = cost t + wa + wb))=>//={a}.
+- by move=>w c a; rewrite inE=>/eqP->; rewrite eq_refl /= !addn0 add0n.
+- move=>_ l r a Hcl _ _ Hal Har IHl _ _.
+  rewrite (notin_alphabet_freq_0 Har) addn0=>Hf.
+  by rewrite (notin_alphabet_splitLeaf_id _ _ _ Har) (weight_splitLeaf _ Hcl Hal Hf) IHl //
+       !addnA (ACl (1*2*5*6*3*4)%AC).
+- move=>_ l r a _ Hcr _ Hal Har _ IHr _.
+  rewrite (notin_alphabet_freq_0 Hal) add0n=>Hf.
+  by rewrite (notin_alphabet_splitLeaf_id _ _ _ Hal) (weight_splitLeaf _ Hcr Har Hf) IHr //
+       !addnA.
+by move=>_ l r a _ _ _ /negbTE Hal /negbTE Har _ _; rewrite !inE Hal Har.
+Qed.
+
+Lemma splitLeafF_insortTree_in_alphabet (t : tree A) ts wa a wb b :
+  a \in alphabet t -> consistent t -> a \notin alphabetF ts -> freq t a = wa + wb ->
+  splitLeafF (insortTree t ts) wa a wb b = insortTree (splitLeaf t wa a wb b) ts.
+Proof.
+move=>Ha Hc + Hf; elim: ts=>//=q s IH; rewrite !inE negb_or; case/andP=>Hq Hs.
+rewrite cachedWeight_splitLeaf; case: ifP=>/= _; rewrite (notin_alphabet_splitLeaf_id _ _ _ Hq).
+- by rewrite (notin_alphabet_splitLeafF_id _ _ _ Hs).
+by rewrite IH.
+Qed.
+
+Lemma splitLeafF_insortTree_in_alphabetF (t : tree A) ts wa a wb b :
+  a \in alphabetF ts -> consistentF ts -> a \notin alphabet t -> freqF ts a = wa + wb ->
+  splitLeafF (insortTree t ts) wa a wb b =
+    insortTree t (splitLeafF ts wa a wb b).
+Proof.
+move=>+ + Ht; elim: ts=>//= u s IH; rewrite !inE=>Ha; case/and3P=>Hi Hu Hs Hf.
+rewrite cachedWeight_splitLeaf; case: ifP=>/= _.
+- by rewrite (notin_alphabet_splitLeaf_id _ _ _ Ht).
+case/boolP: (a \in alphabet u) Ha=>Ha /=; last first.
+- by move=>Has; rewrite IH //; rewrite notin_alphabet_freq_0 in Hf.
+move/alpha_notF: Hi=>/(_ _ Ha) Has _.
+by rewrite !notin_alphabet_splitLeafF_id // alphabetF_insortTree !inE negb_or Ht Has.
+Qed.
+
+(* sortedness *)
+
+Equations sortedByWeight (ts : forest A) : bool :=
+sortedByWeight [::] => true;
+sortedByWeight (t1::ts) with ts := {
+  | [::] => true;
+  | t2 :: _ =>
+    (weight t1 <= weight t2) && (sortedByWeight ts)
+}.
+
+Lemma sortedByWeight_cons2 t1 t2 ts :
+  sortedByWeight (t1::t2::ts) = (weight t1 <= weight t2) && (sortedByWeight (t2::ts)).
+Proof. by simp sortedByWeight. Qed.
+
+Lemma sortedByWeight_cons t ts :
+  sortedByWeight (t::ts) -> sortedByWeight ts.
+Proof. by case: ts=>//=t2 s; rewrite sortedByWeight_cons2; case/andP. Qed.
+
+Lemma sortedByWeight_cons_weight t ts :
+  sortedByWeight (t::ts) -> all (fun u => weight t <= weight u) ts.
+Proof.
+elim: ts t=>//=t2 ts IH t1; rewrite sortedByWeight_cons2.
+case/andP=>H12; rewrite H12 /= => /IH /sub_all; apply=>z Hz.
+by apply/leq_trans/Hz.
+Qed.
+
+Lemma sortedByWeight_insortTree t ts :
+  height t = 0 -> sortedByWeight ts -> heightF ts = 0 ->
+  sortedByWeight (insortTree t ts).
+Proof.
+move=>Ht; funelim (sortedByWeight ts)=>//=.
+- move=>_; rewrite maxn0=>/eqP/heightE [w2][x2]->/=.
+  case: leqP; simp sortedByWeight=>/=; rewrite andbT height_0_cachedWeight //.
+  by move/ltnW.
+case/andP=>Hw Hs /eqP; rewrite !maxn_eq0 .
+case/and3P=>/eqP H1 /eqP H2 Hl; rewrite !height_0_cachedWeight //.
+case: leqP.
+- by rewrite !sortedByWeight_cons2 Hs Hw =>->.
+move=>H10; case: leqP; rewrite !sortedByWeight_cons2.
+- by move/ltnW: H10; rewrite Hs =>->->.
+move=>H20; rewrite Hw /=.
+have Hm: maxn (height t2) (heightF l) = 0.
+- by apply/eqP; rewrite maxn_eq0 Hl andbT; apply/eqP.
+move: (H _ _ Ht erefl Hs Hm)=>/=.
+by rewrite !height_0_cachedWeight // leqNgt H20 /=.
+Qed.
+
+(* minima *)
+
+Definition minima (t : tree A) (a b : A) : bool :=
+  [&& a \in alphabet t,
+      b \in alphabet t,
+      a != b &
+      all (fun c => (c != a) && (c != b) ==>
+                    (freq t a <= freq t c) && (freq t b <= freq t c))
+          (enum t)].
+
+End OtherFunctions.
+
+Section KeyLemmasAndTheorems.
+Context {A : eqType}.
+
+Theorem alphabet_huffman (t0 : tree A) ts :
+  ~~ nilp ts -> alphabet (huffman t0 ts) =i alphabetF ts.
+Proof.
+funelim (huffman t0 ts)=>//; simp huffman=>/= _.
+- by move=>x; rewrite !inE orbF.
+move=>x; rewrite !inE H; last by apply: insortTree_notnil.
+by rewrite alphabetF_insortTree inE /= !inE -orbA.
+Qed.
+
+Theorem consistent_huffman (t0 : tree A) ts :
+  ~~ nilp ts -> consistentF ts -> consistent (huffman t0 ts).
+Proof.
+funelim (huffman t0 ts)=>//; simp huffman=>/= _.
+- by rewrite andbT.
+case/and5P=>Hif H1 Hi2 H2 Hs; apply: H; first by apply: insortTree_notnil.
+rewrite consistentF_insortTree /= -!andbA H1 H2 Hs /= andbT.
+move: Hif; rewrite alpha_intersectsF_cons negb_or; case/andP=>-> Hi1; rewrite andbT.
+by rewrite alpha_intersectsF_uniteTrees negb_or Hi1 Hi2.
+Qed.
+
+Theorem freq_huffman (t0 : tree A) ts a :
+  ~~ nilp ts -> freq (huffman t0 ts) a = freqF ts a.
+Proof.
+funelim (huffman t0 ts)=>//; simp huffman=>/= _.
+- by rewrite addn0.
+rewrite H; last by apply: insortTree_notnil.
+by rewrite freqF_insortTree /= addnA.
+Qed.
+
+(* 13.4 *)
+Lemma cost_swapFourSyms_le (t : tree A) a b c d :
+  consistent t -> minima t a b -> c \in alphabet t -> d \in alphabet t ->
+  depth t c = height t -> depth t d = height t -> c != d ->
+  cost (swapFourSyms t a b c d) <= cost t.
+Proof.
+rewrite /minima=>Hct /and4P [Hat Hbt Hab Hf] Htc Htd Ec Ed Hcd.
+case/boolP: ((a != d) && (b != c)).
+- case/andP=>Had Hbc; rewrite /swapFourSyms (negbTE Had) (negbTE Hbc).
+  case/boolP: (a == c)=>Hac; case/boolP: (b == d)=>Hbd.
+  - rewrite (eqP Hac) (eqP Hbd).
+    have Hd': d \in alphabet (swapSyms t c c) by rewrite alphabet_swapSyms.
+    apply: (leq_trans (n:=cost (swapSyms t c c))); apply: cost_swapSyms_le=>//.
+    by apply: consistent_swapSyms.
+  - rewrite (eqP Hac).
+    apply: (leq_trans (n:=cost (swapSyms t c c))); apply: cost_swapSyms_le=>//.
+    - by apply: consistent_swapSyms.
+    - by rewrite alphabet_swapSyms.
+    - by rewrite alphabet_swapSyms.
+    - rewrite !freq_swapSyms //.
+      move/allP: Hf=>/(_ d); rewrite -alphabet_enum Htd => /(_ erefl).
+      by rewrite eq_sym Had eq_sym Hbd /=; case/andP.
+    rewrite !depth_swapSyms //; try by rewrite eq_sym.
+    by rewrite Ed; apply: depth_le_height.
+  - rewrite (eqP Hbd).
+    apply: (leq_trans (n:=cost (swapSyms t a c))); apply: cost_swapSyms_le=>//.
+    - by apply: consistent_swapSyms.
+    - by rewrite alphabet_swapSyms.
+    - by rewrite alphabet_swapSyms.
+    - move/allP: Hf=>/(_ c); rewrite -alphabet_enum Htc => /(_ erefl).
+      by rewrite eq_sym Hac eq_sym Hbc /=; case/andP.
+    by rewrite Ec; apply: depth_le_height.
+  apply: (leq_trans (n:=cost (swapSyms t a c))); apply: cost_swapSyms_le=>//.
+  - by apply: consistent_swapSyms.
+  - by rewrite alphabet_swapSyms.
+  - by rewrite alphabet_swapSyms.
+  - rewrite !freq_swapSyms //.
+    move/allP: Hf=>/(_ d); rewrite -alphabet_enum Htd => /(_ erefl).
+    by rewrite eq_sym Had eq_sym Hbd /=; case/andP.
+  - rewrite !depth_swapSyms //; try by rewrite eq_sym.
+    by rewrite Ed; apply: depth_le_height.
+  - move/allP: Hf=>/(_ c); rewrite -alphabet_enum Htc => /(_ erefl).
+    by rewrite eq_sym Hac eq_sym Hbc /=; case/andP.
+  by rewrite Ec; apply: depth_le_height.
+rewrite /swapFourSyms negb_and; case/orP=>/negbNE/eqP H.
+- rewrite H in Hab Hf *; rewrite eq_refl.
+  case/boolP: (c == b)=>[/eqP->|Hcb]; first by rewrite swapSyms_id.
+  apply: cost_swapSyms_le=>//.
+  - move/allP: Hf=>/(_ c); rewrite -alphabet_enum Htc => /(_ erefl).
+    by rewrite Hcd Hcb /=; case/andP.
+  by rewrite Ec; apply: depth_le_height.
+rewrite H in Hf *; rewrite eq_refl.
+case/boolP: (a == d)=>[_|Had]; first by rewrite swapSyms_id.
+apply: cost_swapSyms_le=>//.
+- move/allP: Hf=>/(_ d); rewrite -alphabet_enum Htd => /(_ erefl).
+  by rewrite eq_sym Had eq_sym Hcd /=; case/andP.
+by rewrite Ed; apply: depth_le_height.
+Qed.
+
+(* 13.5 *)
+Lemma optimum_splitLeaf (t : tree A) a b wa wb :
+  consistent t -> optimum t ->
+  a \in alphabet t -> b \notin alphabet t ->
+  freq t a = wa + wb ->
+  all (fun c => (wa <= freq t c) && (wb <= freq t c)) (enum t) ->
+  optimum (splitLeaf t wa a wb b).
+Proof.
+move=>Ht Ho Ha Hb Hf H u Hcu.
+set s := splitLeaf t wa a wb b; move=>Hau Hfu.
+case: (posnP (height s))=>[|Hs]; first by case/eqP/heightE=>w[x]->.
+have Hhu : 0 < height u.
+- by apply: (height_gt0_alphabet_eq Hs)=>//; rewrite /s; apply: consistent_splitLeaf.
+have Haau: a \in alphabet u by rewrite -Hau /s alphabet_splitLeaf Ha !inE Ha orbT.
+have Hbau: b \in alphabet u by rewrite -Hau /s alphabet_splitLeaf Ha !inE eq_refl.
+have Hab: a != b by apply/eqP=>E; rewrite -E Ha in Hb.
+case: (exists_at_height Hcu)=>c Hcau Hdc.
+set d := sibling u c.
+have Edc : d != c by rewrite /d; apply: depth_height_sibling_ne.
+have Haad : d \in alphabet u by apply: sibling_ne_in_alphabet.
+set w := swapFourSyms u a b c d.
+have Hcw : consistent w by apply: consistent_swapFourSyms.
+have Haw : alphabet w =i alphabet u by apply: alphabet_swapFourSyms.
+have Hfw : freq w =1 freq u by apply: freq_swapFourSyms.
+have Hsw : sibling w a = b by apply: sibling_swapFourSyms.
+set v := mergeSibling w a.
+have Hav : alphabet v =i alphabet t.
+- move=>z; rewrite alphabet_mergeSibling //; last by rewrite Haw.
+  rewrite !inE Haw Hsw; case: eqP=>[->|_] //=.
+  case: eqP=>[->|/eqP Hzb] /=; first by rewrite (negbTE Hb).
+  by rewrite -Hau alphabet_splitLeaf Ha !inE (negbTE Hzb).
+have Hfv : freq v =1 freq t.
+- move=>z; rewrite freq_mergeSibling //.
+  - rewrite Hsw !Hfw -!Hfu !freq_splitLeaf // !eq_refl Ha (eq_sym b a) (negbTE Hab).
+    case: eqP=>[->|Hza]; first by rewrite Hf.
+    by case: eqP=>// ->; rewrite notin_alphabet_freq_0.
+  - by rewrite Haw -Hau alphabet_splitLeaf Ha !inE Ha orbT.
+  by rewrite Hsw eq_sym.
+rewrite cost_splitLeaf //; apply: (leq_trans (n := cost w)).
+- have <- : cost v + wa + wb = cost w.
+  - have [->->]: wa = freq w a /\ wb = freq w b.
+    - by rewrite !Hfw -!Hfu !freq_splitLeaf // Ha !eq_refl eq_sym (negbTE Hab).
+    by rewrite -Hsw cost_mergeSibling // Hsw eq_sym.
+  by rewrite -!addnA leq_add2r; apply: Ho=>//; apply: consistent_mergeSibling.
+have Hm : minima u a b.
+- rewrite /minima Haau Hbau Hab /=; apply/allP=>z.
+  rewrite -alphabet_enum -Hau alphabet_splitLeaf Ha !inE.
+  case/orP; first by move=>-> /=; rewrite andbF.
+  rewrite alphabet_enum; move/allP: H=>/[apply]; case/andP=>Hwaz Hwbz.
+  apply/implyP; case/andP=>Hza Hzb; rewrite -!Hfu !freq_splitLeaf // Ha.
+  by rewrite !eq_refl (negbTE Hza) (negbTE Hzb) eq_sym (negbTE Hab) Hwaz Hwbz.
+by apply: cost_swapFourSyms_le=>//; [rewrite depth_sibling | rewrite eq_sym].
+Qed.
+
+(* 13.6 *)
+Lemma splitLeaf_huffman_commute (t0 : tree A) ts wa a wb b :
+ consistentF ts -> ~~ nilp ts -> a \in alphabetF ts -> freqF ts a = wa + wb ->
+ splitLeaf (huffman t0 ts) wa a wb b = huffman t0 (splitLeafF ts wa a wb b).
+Proof.
+funelim (huffman t0 ts); simp huffman=>//=; simp huffman.
+rewrite alpha_intersectsF_cons negb_or -andbA; case/and6P=>Hi12 Hi1s Hc1 Hi2s Hc2 Hcs _.
+rewrite !inE=>Ha Hf; rewrite H.
+- rewrite /uniteTrees /= !cachedWeight_splitLeaf.
+  case/or3P: Ha=>Ha.
+  - move/alpha_notF: Hi1s=>/(_ _ Ha)=>Has.
+    rewrite splitLeafF_insortTree_in_alphabet //=.
+    - by rewrite notin_alphabet_splitLeafF_id.
+    - by rewrite !inE Ha.
+    - by rewrite Hi12 Hc1 Hc2.
+    by move: Hf; rewrite notin_alphabet_freqF_0 // addn0.
+  - move/alpha_notF: Hi2s=>/(_ _ Ha)=>Has.
+    rewrite splitLeafF_insortTree_in_alphabet //=.
+    - by rewrite notin_alphabet_splitLeafF_id.
+    - by rewrite !inE Ha orbT.
+    - by rewrite Hi12 Hc1 Hc2.
+    by move: Hf; rewrite notin_alphabet_freqF_0 // addn0.
+  move/alpha_notFC: Hi1s=>/(_ _ Ha)=>Ha1.
+  move/alpha_notFC: Hi2s=>/(_ _ Ha)=>Ha2.
+  rewrite splitLeafF_insortTree_in_alphabetF //=.
+  - by rewrite !notin_alphabet_splitLeaf_id.
+  - by rewrite !inE negb_or Ha1 Ha2.
+  by move: Hf; rewrite !notin_alphabet_freq_0.
+- by rewrite consistentF_insortTree /= alpha_intersectsF_uniteTrees negb_or
+       Hi1s Hi2s Hi12 Hc1 Hc2 Hcs.
+- by apply: insortTree_notnil.
+- by rewrite alphabetF_insortTree /uniteTrees /= !inE -orbA.
+by rewrite freqF_insortTree /uniteTrees /= -addnA.
+Qed.
+
+(* 13.7 *)
+Theorem optimum_huffman (t0 : tree A) ts :
+  consistentF ts -> heightF ts = 0 -> sortedByWeight ts -> ~~ nilp ts ->
+  optimum (huffman t0 ts).
+Proof.
+elim/(@size_ind (tree A)): ts=>[xs|n IH xs Hs].
+- by move/size0nil=>->.
+case: xs Hs=>//= t1; case=>[_|t2 ts] /=.
+- move=>_; simp sortedByWeight huffman.
+  by rewrite maxn0=>/eqP/heightE [w][x] ->.
+rewrite ltnS alpha_intersectsF_cons negb_or -andbA =>Hs.
+case/and6P=>Hi12 Hi1s _ Hi2s _ Hcs; simp huffman.
+move/eqP; rewrite !maxn_eq0; case/and3P=>Hh1 Hh2 Hhs.
+move/heightE: Hh1=>[wa][a] Ea; move/heightE: Hh2=>[wb][b] Eb.
+rewrite {t1}Ea {t2}Eb /uniteTrees /alpha_intersectsF /alpha_intersects /= ?orbF in Hi12 Hi1s Hi2s *.
+move/[dup]=>/sortedByWeight_cons_weight /=; case/andP=>_ Haw1.
+move/sortedByWeight_cons/[dup]=>/sortedByWeight_cons_weight /= Haw2.
+move/sortedByWeight_cons=>Hsw _.
+have Haas: a \notin alphabetF ts.
+- move: Hi1s; rewrite alphabet_enumF.
+  by move/hasPn=>H; apply/negP=>/H; rewrite inE eq_refl.
+have {Hi2s}Hbas: b \notin alphabetF ts.
+- move: Hi2s; rewrite alphabet_enumF.
+  by move/hasPn=>H; apply/negP=>/H; rewrite inE eq_refl.
+have {Hi1s}Hci : consistentF (insortTree (Leaf (wa + wb) a) ts).
+- by rewrite consistentF_insortTree /= Hcs andbT.
+have Hni : ~~ nilp (insortTree (Leaf (wa + wb) a) ts).
+- by apply: insortTree_notnil.
+have -> : huffman t0 (insortTree (Node (wa + wb) (Leaf wa a) (Leaf wb b)) ts) =
+          splitLeaf (huffman t0 (insortTree (Leaf (wa + wb) a) ts)) wa a wb b.
+- rewrite splitLeaf_huffman_commute //.
+  - by rewrite splitLeafF_insortTree_in_alphabet /= ?eq_refl // inE eq_refl.
+  - by rewrite alphabetF_insortTree !inE eq_refl.
+  by rewrite freqF_insortTree /= eq_refl notin_alphabet_freqF_0 // addn0.
+apply: optimum_splitLeaf; first by apply: consistent_huffman.
+- apply: IH=>//; first by rewrite size_insortTree.
+  - by rewrite heightF_insortTree; apply/eqP; rewrite maxn_eq0.
+  by apply: sortedByWeight_insortTree=>//; apply/eqP.
+- by rewrite alphabet_huffman=>//; rewrite alphabetF_insortTree !inE eq_refl.
+- by rewrite alphabet_huffman=>//; rewrite alphabetF_insortTree !inE negb_or Hi12.
+- by rewrite freq_huffman // freqF_insortTree /= eq_refl notin_alphabet_freqF_0 // addn0.
+apply/allP=>z; rewrite -alphabet_enum alphabet_huffman // alphabetF_insortTree !inE
+                 freq_huffman // freqF_insortTree /=; case/orP=>[/eqP->|Hz].
+- by rewrite eq_refl notin_alphabet_freqF_0 // addn0 leq_addr leq_addl.
+move: (heightF_0_Leaf_freqF Hcs (eqP Hhs) Hz)=>Hl.
+case: eqP=>[Ez|_]; first by rewrite -Ez Hz in Haas.
+by rewrite add0n; move/allP: Haw1=>/(_ _ Hl); move/allP: Haw2=>/(_ _ Hl) /=->->.
+Qed.
+
+End KeyLemmasAndTheorems.