proposition: Lemma size_add_ribbon : size res = maxn (size sh) pos.+1.
proof: Proof. move: Hret; rewrite /add_ribbon. move: (startrem_leq sh nbox.+1 pos). case: startrem => start [|rem]//= /(_ (ltn0Sn _)) lesmin [<- _]. have:= lesmin; rewrite leq_min => /andP[lespos lessz]. rewrite /add_ribbon_on !size_cat /= size_map size_nseq. rewrite !size_drop !size_take. rewrite addSnnS -addSn -!/(minn _ _) (minn_idPl lessz). rewrite addnA subnKC //. case: (ltnP pos (size sh)) => [Hlt|Hge]. have:= ltnW Hlt; rewrite -subn_eq0 => /eqP ->. by rewrite addn0 -subSn // subSS (subnKC (ltnW Hlt)) (maxn_idPl Hlt). have:= Hge; rewrite -ltnS => /ltnW; rewrite -subn_eq0 => /eqP -> /=. by rewrite add1n -subSn // maxnE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition