proposition: Lemma dnicommsq ( n : nat ) ( i : ⟦S n⟧ ) : commsqstr( dni i ) ( stntonat ( S n ) ) ( stntonat n ) ( di i ).
proof: Proof. intros. intro x. unfold dni. unfold di. destruct ( natlthorgeh x i ). - simpl. apply idpath. - simpl. apply idpath. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions