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