proposition: Lemma isdecinclstntonat ( n : nat ) : isdecincl ( stntonat n ).
proof: Proof. intro. use isdecinclpr1. intro x. apply isdecpropif. use pr2. apply isdecrelnatgth. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions