Lemma isincldi (i : nat) : isincl (di i). Proof. intro. apply (isinclbetweensets (di i) isasetnat isasetnat). intros x x'. unfold di. intro e. induction (natlthorgeh x i) as [ l | nel ]. - induction (natlthorgeh x' i) as [ l' | nel' ]. + apply e. + rewrite e in l. assert (e' := natgthtogths _ _ l). change (S i > S x') with (i > x') in e'. contradicts (natlehtonegnatgth _ _ nel') e'. - induction (natlthorgeh x' i) as [ l' | nel' ]. + induction e. set (e' := natgthtogths _ _ l'). contradicts (natlehtonegnatgth _ _ nel) e'. + apply (invmaponpathsS _ _ e). Defined.