Lemma isdecinclnatplusr (n : nat) : isdecincl (λ i : nat, i + n). Proof. intros. intro m. apply isdecpropif. - apply (isinclnatplusr _ m). - induction (natlthorgeh m n) as [ ni | i ]. + apply (ii2 (neghfibernatplusr n m ni)). + apply (ii1 (pr1 (iscontrhfibernatplusr n m i))). Defined.