proposition: Lemma ribbon_on_startE : start = mindropeq inner outer - ribbon_height inner outer.
proof: Proof. rewrite ribbon_on_mindropeq -ribbon_on_height. by rewrite subSS subKn // ribbon_on_start_stop. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition