Lemma neghfiberdi (i : nat) : ¬ (hfiber (di i) i). Proof. intros hf. unfold di in hf. induction hf as [ j e ]. induction (natlthorgeh j i) as [ l | g ]. induction e. apply (isirreflnatlth _ l). induction e in g. apply (negnatgehnsn _ g). Defined.