proposition: Lemma ribbon_addE inner outer : is_part inner -> is_part outer -> ribbon inner outer -> add_ribbon inner (sumn (outer / inner)).-1 (mindropeq inner outer).-1 = Some (outer, ribbon_height inner outer).
proof: Proof. move=> partinn partout Hrib. have:= Hrib => /(ribbonP partinn partout) [start][stop] Hrib_on. rewrite -(ribbon_on_stopE partinn partout Hrib_on). rewrite /add_ribbon (ribbon_sumn_diffE partout Hrib). rewrite (ribbon_on_startrem partinn partout Hrib_on) subn_gt0. have := Hrib_on => [][_ _ -> _]; congr (Some (_, _)); first last. by rewrite (ribbon_on_height partinn partout). exact: ribbon_on_addE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition