proposition: Lemma intpart_rem_corner_ind (F : intpart -> Type) : F empty_intpart -> (forall p : intpart, (forall i, is_rem_corner p i -> F (decr_nth_intpart p i)) -> F p) -> forall p : intpart, F p.
proof: Proof. move=> H0 Hrec p. move Hp : (sumn p) => n. elim: n p Hp => [| n IHn] p Hp; first by rewrite (empty_intpartP Hp). apply: Hrec => i Hi. apply: IHn; rewrite /decr_nth_intpart /= Hi. by rewrite (sumn_decr_nth (intpartP p) Hi) Hp. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype