Theorem isaprople (n m : nat) : isaprop (le n m). Proof. intros. apply (isofhlevelweqb 1 (weqleFtototalwithnat S n m)). apply invproofirrelevance. intros x x'. set (i := @pr1 _ (λ n0 : nat, (iteration S n0 n) = m)). assert (is : isincl i) by apply (isinclpr1 _ (λ n0 : nat, isasetnat (iteration S n0 n) m)). apply (invmaponpathsincl _ is). destruct x as [ n1 e1 ]. destruct x' as [ n2 e2 ]. simpl. set (int1 := pathsinv0 (pathsitertoplus n1 n)). set (int2 := pathsinv0 (pathsitertoplus n2 n)). set (ee1 := pathscomp0 int1 e1). set (ee2 := pathscomp0 int2 e2). set (e := pathscomp0 ee1 (pathsinv0 ee2)). apply (invmaponpathsincl _ (isinclnatplusr n) n1 n2 e). Defined.