proposition: Lemma ribbon_from_noneq inner outer : ribbon_from inner outer -> inner != outer.
proof: Proof. case: inner outer => [| inn0 inn] [| out0 out] //=. by rewrite eqseq_cons => /andP[/ltn_eqF ->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition