Lemma iscontrhfibernatplusl (n m : nat) (is : m ≥ n) : iscontr (hfiber (λ i : nat, n + i) m). Proof. intros. apply iscontraprop1. - apply isinclnatplusl. - induction m as [ | m IHm ]. + set (e := natleh0tois0 is). split with 0. rewrite natplusr0. apply e. + induction (natlehchoice2 _ _ is) as [ l | e ]. * set (j := IHm l). induction j as [ j e' ]. split with (S j). simpl. rewrite <- plus_n_Sm. apply (maponpaths S e'). * split with 0. simpl. rewrite natplusr0. assumption. Defined.