proposition: Lemma ribbon_from_mindropeq inner outer : is_part inner -> is_part outer -> ribbon_from inner outer -> ribbon_on 0 (mindropeq inner outer).-1 inner outer.
proof: Proof. move=> partinn partout /(ribbon_fromP partinn partout) [stop] Hrib. by rewrite -(ribbon_on_stopE partinn partout Hrib). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition