proposition: Lemma corner_box_conj_part sh u v : is_part sh -> corner_box sh (u, v) -> corner_box (conj_part sh) (v, u).
proof: Proof. rewrite /corner_box {1}/is_rem_corner => Hpart /= /andP[Hcorn /eqP->{v}]. rewrite (rem_corner_conj_part Hpart Hcorn) /= eq_sym. have : nth 0 sh u.+1 <= (nth 0 sh u).-1 < (nth 0 sh u). move: Hcorn; case: (nth 0 sh u) => [// | shu]. by rewrite ltnS [shu.+1.-1]/= => -> /=. by rewrite -nth_conjE // => /eqP -> /=. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure