proposition: Lemma isweqdnitocompl ( n : nat ) ( i : ⟦S n⟧ ) : isweq ( dnitocompl n i ).
proof: Proof. intros jni. assert ( w := samehfibers ( dnitocompl n i ) _ ( isinclpr1compl_ne _ i _ ) jni ) ; simpl in w. apply (iscontrweqb w). apply iscontrhfiberdni. exact (pr2 jni). Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions