proposition: Lemma ribbon_fromP inner outer : is_part inner -> is_part outer -> reflect (exists stop, ribbon_on 0 stop inner outer) (ribbon_from inner outer).
proof: Proof. rewrite /ribbon_on=> Hinn Hout; apply (iffP idP); elim: inner Hinn outer Hout => [| inn0 inn IHinn] Hinn [|out0 out] Hout //=. - move=> H; exists (size out) => /=. move/(part_nseq1P (is_part_consK Hout)) : H ->; rewrite size_nseq. split => //[i Hi | i Hi | ]. + by rewrite nth_nil nth_default //= size_nseq. + by rewrite nth_nil nth_nseq Hi. + by move/part_head_non0 : Hout => /=; rewrite lt0n. - move=> /andP[lt0 /orP[/eqP -> | /andP[/eqP Hhead Hrib]]]/=. + by exists 0; split=> //; case. + move: Hinn Hout => /=/andP[headinn Hinn] /=/andP[headout Hout]. move/(_ Hinn _ Hout Hrib): IHinn => [stop [Hsi His H0 _]]. by exists stop.+1; split=> []// [|i] Hi //=; [exact: Hsi| exact: His]. - by move=> [stop []]. - move=> [[|stop] [His Hsi _]]. by have:= His 1 (ltnSn _); rewrite /= nth0 => ->. by have:= Hsi 0 (ltn0Sn _); rewrite /= nth0 => ->. - by move=> [stop []]. - move=> [stop [Hsi His H0 _]]; rewrite H0 /=. case Hneq: (out == inn) => //=. move: Hinn Hout => /=/andP[headinn Hinn] /=/andP[headout Hout]. case: stop => [|stop] in Hsi His. exfalso => {His}; move: Hneq; suff -> : out = inn by rewrite eqxx. by apply/eqP/part_eqP => // i; apply: Hsi i.+1 (ltn0Sn _). have /= <- := His 0 (ltn0Sn _); rewrite nth0 eqxx /=. apply: IHinn => //; exists stop; split => // [i Hi|i Hi|]. + exact: (Hsi i.+1 Hi). + exact: (His i.+1 Hi). + have /= -> := His 0 (ltn0Sn _); rewrite nth0 ltnS. by move: headinn; case inn. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition