proposition: Lemma hzgthtogehsn ( n m : hz ) : hzgth n m -> hzgeh n ( m + 1 ) .
proof: Proof. assert ( int : ∏ n m , isaprop ( hzgth n m -> hzgeh n ( m + 1 ) ) ) . { intros . apply impred . intro . apply ( pr2 _ ) . } unfold hzgth in * . apply ( setquotuniv2prop _ ( λ n m, make_hProp _ ( int n m ) ) ) . set ( R := abgrdiffrelint nataddabmonoid natgth ) . intros x x' . change ( R x x' -> ( neg ( R ( @op ( abmonoiddirprod (rigaddabmonoid natcommrig) (rigaddabmonoid natcommrig) ) x' ( make_dirprod 1%nat 0%nat ) ) x ) ) ) . unfold R . unfold abgrdiffrelint . simpl . apply ( @hinhuniv _ (make_hProp ( neg ( ishinh_UU _ ) ) ( isapropneg _ ) ) ) . intro t2 . simpl . unfold neg . apply ( @hinhuniv _ ( make_hProp _ isapropempty ) ) . intro t2' . set ( x1 := pr1 x ) . set ( a1 := pr2 x ) . set ( x2 := pr1 x' ) . set ( a2 := pr2 x' ) . set ( c1 := pr1 t2 ) . assert ( r1 := pr2 t2 ) . change ( pr1 ( ( x1 + a2 + c1 ) > ( x2 + a1 + c1 ) ) ) in r1 . set ( c2 := pr1 t2' ) . assert ( r2 := pr2 t2' ) . change ( pr1 ( ( ( x2 + 1 ) + a1 + c2 ) > ( x1 + ( a2 + 0 ) + c2 ) ) ) in r2 . assert ( r1' := natgthandplusrinv _ _ c1 r1 ) . assert ( r2' := natgthandplusrinv _ _ c2 r2 ) . rewrite ( natplusr0 _ ) in r2' . rewrite ( natpluscomm _ 1 ) in r2' . rewrite ( natplusassoc _ _ _ ) in r2' . change (1 + (x2 + a1) > x1 + a2) with (x1 + a2 ≤ x2 + a1) in r2'. contradicts (natlehneggth r2') r1'. Defined . Lemma hzgthsntogeh ( n m : hz ) : hzgth ( n + 1 ) m -> hzgeh n m . Proof. intros a . apply (hzgehandplusrinv n m 1) . apply ( hzgthtogehsn ( n + 1 ) m a ) . Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra