Lemma apartbinarysum0 ( R : acommring ) ( a b : R ) ( p : a + b # 0 ) : a # 0 ∨ b # 0. Proof. intros. intros P s. use ( hinhuniv _ ( acommring_acotrans R ( a + b ) a 0 p ) ). intro k. destruct k as [ l | r ]. - apply s. apply ii2. assert ( a + b # a ) as l' by apply l. assert ( ( a + b ) # ( a + 0 ) ) as l''. { rewrite ringrunax1. assumption. } apply ( pr1 ( acommring_aadd R ) a b 0 ). assumption. - apply s. apply ii1. assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.NumberSystems.Integers.