proposition: Lemma sumn_right_sizes_gt t t' : t' \in rotations t -> sumn (right_sizes t) < sumn (right_sizes t').
proof: Proof. elim: t t' => // l IHl r IHr t'. case Hl : l IHl => [| ll lr] IHl. rewrite /= => /mapP[/= rot Hrot ->{t'}] /=. rewrite (size_rotations Hrot) ltn_add2l. exact: IHr. rewrite -Hl /= {1}Hl /= inE => /orP[/eqP-> /=|]. do 2 rewrite !sumn_cat /=; rewrite Hl /= !sumn_cat /= addnA. rewrite add1n !(addSn, addnS) ltnS -!addnA !leq_add2l !addnA !leq_add2r. exact: leq_addl. rewrite -Hl in IHl. rewrite mem_cat => /orP[/mapP[/= lrot Hlrot] | /mapP[/= rrot Hrrot]] -> /=. - rewrite !sumn_cat /= ltn_add2r. exact: IHl. - rewrite (size_rotations Hrrot) !sumn_cat /= !ltn_add2l. exact: IHr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools combclass ordtype