proposition: Lemma psi_diff e1 e2 : psi e1 - psi e2 <= \sum_(i <- e1 `\` e2) 2 ^ troot i.
proof: Proof. rewrite leq_subLR -(ler_nat (Num.NumDomain.clone _ int)) natrD addrC -lerBlDr. have [l ->] := psiE e1. apply: le_trans (lerB (lexx _) (psi_max _ l)) _. rewrite /psi_aux opprB addrA subrK addnC !natrD opprD addrA addrK. rewrite lerBlDr -natrD ler_nat addnC -leq_subLR. set s1 := \sum_(_ <- _) _; set s2 := \sum_(_ <- _) _; set s3 := \sum_(_ <- _) _. pose f i := 2 ^ minn (troot i) l. apply: leq_trans (_ : \sum_(i <- e1 `\` e2) f i <= _); last first. by apply: leq_sum => i _; rewrite leq_exp2l // geq_minl. rewrite leq_subLR. rewrite [s1](big_fsetID _ (fun i => i \in e2)) //=. apply: leq_add. rewrite [s2](big_fsetID _ (fun i => i \in e1)) //=. apply: leq_trans (leq_addr _ _). rewrite leq_eqVlt; apply/orP; left; apply/eqP. by apply: eq_fbigl => i; rewrite !inE andbC. rewrite leq_eqVlt; apply/orP; left; apply/eqP. by apply: eq_fbigl => i; rewrite !inE andbC. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) hanoi(extra triangular phi)