Lemma natcofaceretractisretract ( i : nat ) : funcomp ( natcoface i ) ( natcofaceretract i ) = idfun nat. Proof. simpl. apply funextfun. intro n. simpl. set ( c := natlthorgeh n i ). destruct c as [ h | k ]. - unfold natcoface. rewrite h. unfold natcofaceretract. rewrite h. apply idpath. - assert ( natgtb i n = false ) as f. { apply natgehimplnatgtbfalse. assumption. } unfold natcoface. rewrite f. unfold natcofaceretract. assert ( natgtb i ( S n ) = false ) as ff. { apply natgehimplnatgtbfalse. apply ( istransnatgeh _ n ). + apply natgthtogeh. apply natgthsnn. + assumption. } rewrite ff. rewrite minussn1. apply idpath. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Algebra.Monoids.