proposition: Lemma ribbon_on0_startrem stop inner outer acc : is_part inner -> is_part outer -> ribbon_on 0 stop inner outer -> startrem acc inner (sumn (outer / inner)) stop = (acc, nth 0 outer 0 - nth 0 inner 0).
proof: Proof. move=> partinn partout Hrib. case: outer partout Hrib => [_ [_ _] | out0 out]; first by rewrite nth_nil. case: inner partinn => [|inn0 inn]. move => _ /=/andP[Hout0 partout] [Hsi His]. rewrite nth_nil /= => H0 _; rewrite !subn0. case: stop Hsi His => [|st /= Hsi His]. case: out partout {Hout0} => [|out1 out]. by move=> _ _ _; rewrite !(sub0n, addn0, subn0). move=> /part_head_non0 /= /negbTE Hout1 /(_ 1 (ltnSn 0)) /= /eqP. by rewrite Hout1. suff -> : out = nseq st.+1 1. rewrite sumn_nseq mul1n; have := leq_addl out0 st.+1. by rewrite -subn_eq0 => /eqP ->; rewrite addn0 addnK. apply/eqP/(part_eqP partout (is_part_nseq1 _)) => i. rewrite nth_nseq; case: ltnP => [/His ->|]; first by rewrite nth_nil. by rewrite -ltnS => /Hsi /=. move=> partinn partout Hrib. rewrite (ribbon_on_sumn partinn partout Hrib) subn0 /=. case: stop Hrib => [|st] [Hsi Hsis /= H0 _]. by rewrite sub0n addn0 subn0 add0n. rewrite [st.+1 + _]addnC !addnA leq_add2r subnKC ?(ltnW H0) /=; first last. apply: (leq_trans _ (ltnW H0)). by move: partinn => /is_part_ijP[_] /(_ _ _ (leq0n st.+1)) /=. by rewrite subnDr. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition