Lemma leastelementprinciple ( n : nat ) ( P : nat -> hProp ) ( is : isdecnatprop P ) : P n -> ∃ k : nat, P k × forall m : nat, natlth m k -> neg ( P m ). Proof. revert P is. induction n. - intros P is u. apply total2tohexists. split with 0%nat. split. + assumption. + intros m i. apply fromempty. apply ( negnatgth0n m i ). - intros P is u. destruct ( is 0%nat ) as [ l | r ]. + apply total2tohexists. split with 0%nat. split. * assumption. * intros m i. apply fromempty. apply ( negnatgth0n m i ). + set ( P' := fun m : nat => P ( S m ) ). assert ( forall m : nat, P' m ⨿ neg ( P' m ) ) as is'. { intros m. unfold P'. apply ( is ( S m ) ). } set ( c := IHn P' is' u ). use (hinhuniv _ c). intros k. destruct k as [ k v ]. destruct v as [ v0 v1 ]. apply total2tohexists. split with ( S k ). split. * assumption. * intros m. destruct m. -- intros i. assumption. -- intros i. apply v1. apply i. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Algebra.Monoids.