fact: Fixpoint ribbon inner outer := ribbon_from inner outer || if (inner, outer) is (inn0 :: inn, out0 :: out) then (out0 == inn0) && (ribbon inn out) else false.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition