Lemma apartnatsummation0 ( R : acommring ) ( upper : nat ) ( f : nat -> R ) ( p : ( natsummation0 upper f ) # 0 ) : ∃ n : nat, natleh n upper × f n # 0. Proof. revert f p. induction upper. - simpl. intros. intros P s. apply s. split with 0%nat. split. + apply idpath. + assumption. - intros. intros P s. simpl in p. use ( hinhuniv _ (apartbinarysum0 R _ _ p ) ). intro k. destruct k as [ l | r ]. + use ( hinhuniv _ (IHupper f l ) ). intro k. destruct k as [ n ab ]. destruct ab as [ a b ]. apply s. split with n. split. * apply ( istransnatleh( m := upper ) ). -- assumption. -- apply natlthtoleh. apply natlthnsn. * assumption. + apply s. split with ( S upper ). split. * apply isreflnatleh. * assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.