proposition: Lemma ribbon_noneq inner outer : ribbon inner outer -> outer != inner.
proof: Proof. elim: inner outer => [| inn0 inn IHinn] [| out0 out] //=. by rewrite eqseq_cons => /orP[/andP[/gtn_eqF ->] // | /andP[-> /IHinn]]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition