proposition: Lemma ribbon_onSS start stop inn0 inn out0 out : ribbon_on start.+1 stop.+1 (inn0 :: inn) (out0 :: out) <-> inn0 == out0 /\ ribbon_on start stop inn out.
proof: Proof. rewrite /ribbon_on; split => [ |[/eqP ->]] [Hsi Hsis Hs His]. - split; first exact/eqP/esym/(His _ (ltn0Sn _)). split=> // i Hi; [exact: (Hsi i.+1) | exact: (Hsis i.+1) | exact: (His i.+1)]. - split=> //-[|i] Hi//=; [exact: Hsi | exact: Hsis | exact: His]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition