Lemma iscontrhfiberdi (i j : nat) (ne : i ≠ j) : iscontr (hfiber (di i) j). Proof. intros. apply iscontraprop1. apply (isincldi i j). induction (natlthorgeh j i) as [ l | nel ]. - split with j. unfold di. induction (natlthorgeh j i) as [ l' | nel' ]. + apply idpath. + contradicts (natlehtonegnatgth _ _ nel') l. - induction (natgehchoice2 _ _ nel) as [ g | e ]. destruct j as [ | j ]. + induction (negnatgeh0sn _ g). + split with j. unfold di. induction (natlthorgeh j i) as [ l' | g' ]. * contradicts (natlehtonegnatgth _ _ g) l'. * apply idpath. + induction ((nat_neq_to_nopath ne) (pathsinv0 e)). Defined.