proposition: Lemma ribbon_consK inn0 inn out0 out : ribbon (inn0 :: inn) (out0 :: out) -> (out == inn) || ribbon inn out.
proof: Proof. by move=>/=/orP[/andP[_ /orP[-> //| /andP[_ /ribbon_from_impl->]]] | /andP[_ ->]]; rewrite orbT. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition