proposition: Lemma hzlehsntolth ( n m : hz ) : hzleh ( n + 1 ) m -> hzlth n m .
proof: Proof. intros X . apply ( hzlthlehtrans _ _ _ ( hzlthnsn n ) X ) . Defined . Lemma hzlthtolehsn ( n m : hz ) : hzlth n m -> hzleh ( n + 1 ) m . Proof. intros X . apply ( hzgthtogehsn m n X ) . Defined . Lemma hzlthsntoleh ( n m : hz ) : hzlth n ( m + 1 ) -> hzleh n m . Proof. intros a . apply (hzlehandplusrinv n m 1) . apply ( hzlthtolehsn n ( m + 1 ) a ) . Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra