proposition: Lemma natcofaceretractisretract ( i : nat ) : funcomp ( natcoface i ) ( natcofaceretract i ) = idfun nat.
proof: 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.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.NumberSystems.Integers UniMath.Algebra.Monoids