proposition: Lemma ribbon_on_mindropeq : mindropeq inner outer = stop.+1.
proof: Proof. move: partinn partout => /notin0_part inn0 /notin0_part out0. apply/eqP/(mindropeq_nthP _ inn0 out0) => {inn0 out0}. split => [|i]; last by move: Hrib => [Hsi _ _ _] /Hsi ->. rewrite ltn_eqF // -ribbon_on_nth_leq. by rewrite ribbon_on_start_stop leqnn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition