Lemma isinclnatplusr (n : nat) : isincl (λ m : nat, m + n). Proof. induction n as [ | n IHn ]. - apply (isofhlevelfhomot 1 _ _ (λ m : nat, pathsinv0 (natplusr0 m))). apply (isofhlevelfweq 1 (idweq nat)). - apply (isofhlevelfhomot 1 _ _ (λ m : nat, pathsinv0 (natplusnsm m n))). simpl. apply (isofhlevelfgf 1 _ _ isinclS IHn). Defined.