proposition: Lemma hook_length1_corner sh rc : is_part sh -> in_shape sh rc -> hook_length sh rc = 1 -> corner_box sh rc.
proof: Proof. move: rc => [r c] Hpart. rewrite /in_shape /= => Hin_part /eqP. rewrite /hook_length eqSS addn_eq0 => /andP[Hnth Hhaut]. apply /andP; split. - rewrite /is_rem_corner/=. apply: (leq_trans _ Hin_part). rewrite ltnS (conj_leqE Hpart). by rewrite -subn_eq0 subnS. - rewrite eqn_leq; apply /andP; split. + rewrite -ltnS; apply (leq_trans Hin_part). exact: leqSpred. + by rewrite -subn_eq0 -subn1 -subnAC subn1. Qed.
imports: Misc Ccpo mathcomp(all_ssreflect) mathcomp(ssrint div rat ssralg ssrnum) tools subseq partition Yamanouchi stdtab Qmeasure