proposition: Lemma ribbon_on_height : (stop - start).+1 = ribbon_height inner outer.
proof: Proof. rewrite /ribbon_height -sumn_count sumnE big_map (big_nth 0) size_diff_shape. rewrite (big_cat_nat _ _ _ (leq0n start) (leq_trans ribbon_on_start_stop (ltnW ribbon_on_stop_lt))) /=. rewrite big_nat big1 ?add0n; first last => [i /= leis|]. rewrite nth_diff_shape subn_gt0 -ribbon_on_nth_leq. by rewrite leqNgt leis. have := ribbon_on_start_stop; rewrite -ltnS => leqss. rewrite (big_cat_nat _ _ _ (ltnW leqss) ribbon_on_stop_lt) /= addnC. rewrite big_nat big1 ?add0n; first last => [i /= /andP[ltsi _]|]. rewrite nth_diff_shape subn_gt0 -ribbon_on_nth_leq. by rewrite (leqNgt i) ltsi andbF. rewrite big_nat; under eq_bigr => i. rewrite ltnS ribbon_on_nth_leq nth_diff_shape subn_gt0 => -> /=. by rewrite over. by rewrite /= -big_nat sum_nat_const_nat muln1 subSn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition