proposition: Lemma part_rem_corner_ind (F : seq nat -> Type) : F [::] -> (forall p, is_part p -> (forall i, is_rem_corner p i -> F (decr_nth p i)) -> F p) -> forall p, is_part p -> F p.
proof: Proof. move=> H0 Hrec p Hp; rewrite -[p]/(val (IntPart Hp)). apply: (intpart_rem_corner_ind (F := fun p => F (val p))) => [//|{Hp}p IHp]. apply (Hrec p (intpartP p)) => i Hi. by move/(_ i Hi): IHp; rewrite /= Hi. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype