Theorem weqdicompl (i : nat) : nat ≃ nat_compl i. Proof. use weq_iso. - intro j. exists (di i j). apply di_neq_i. - intro j. exact (si i (pr1 j)). - simpl. intro j. unfold di. induction (natlthorgeh j i) as [lt|ge]. + unfold si. induction (natlthorgeh i j) as [lt'|ge']. * contradicts (isasymmnatlth _ _ lt') lt. * apply idpath. + unfold si. induction (natlthorgeh i (S j)) as [lt'|ge']. * change (S j) with (1 + j). rewrite natpluscomm. apply plusminusnmm. * unfold natgeh,natleh in ge. contradicts (natlehneggth ge') ge. - simpl. intro j. induction j as [j ne]; simpl. apply subtypePath. + intro k. apply negProp_to_isaprop. + simpl. unfold si. induction (natlthorgeh j i) as [lt|ge]. * clear ne. induction (natlthorgeh i j) as [lt'|_]. { contradicts (isasymmnatlth _ _ lt') lt. } { unfold di. induction (natlthorgeh j i) as [lt'|ge']. - apply idpath. - contradicts (natgehtonegnatlth _ _ ge') lt. } * assert (lt := natleh_neq ge ne); clear ne ge. induction (natlthorgeh i j) as [_|ge']. { unfold di. induction (natlthorgeh (j - 1) i) as [lt'|ge']. - apply fromempty. induction j as [|j _]. + exact (negnatlthn0 _ lt). + change (S j) with (1 + j) in lt'. rewrite natpluscomm in lt'. rewrite plusminusnmm in lt'. change (i < S j) with (i ≤ j) in lt. exact (natlehneggth lt lt'). - induction j as [|j _]. + contradicts (negnatlthn0 i) lt. + simpl. apply maponpaths. apply natminuseqn. } contradicts (natgehtonegnatlth _ _ ge') lt. Defined.