Lemma neghfibernatplusr (n m : nat) (is : m < n) : ¬ (hfiber (λ i : nat, i + n) m). Proof. intros. intro h. induction h as [ i e ]. rewrite (pathsinv0 e) in is. induction (natlehtonegnatgth _ _ (natlehmplusnm i n) is). Defined.