proposition: Lemma isinclhzplusl ( n : hz ) : isincl ( λ m : hz, n + m ) .
proof: Proof. apply ( pr2 ( weqtoincl ( weqlmultingr hzaddabgr n ) ) ) . Defined . Lemma hzpluslcan ( a b c : hz ) ( is : ( c + a ) = ( c + b ) ) : a = b . Proof . intros . apply ( @grlcan hzaddabgr a b c is ) . Defined . Lemma hzplusrcan ( a b c : hz ) ( is : ( a + c ) = ( b + c ) ) : a = b . Proof . intros . apply ( @grrcan hzaddabgr a b c is ) . Defined . Definition hzinvmaponpathsminus { a b : hz } ( e : ( - a ) = ( - b ) ) : a = b := grinvmaponpathsinv hzaddabgr e . Lemma hzrplusminus (n m : hz) : n + m - m = n. Proof. unfold hzminus, hzplus, hzplus. rewrite ringassoc1. set (tmp := hzrminus m). unfold hzminus, hzplus in tmp. rewrite tmp. clear tmp. apply hzplusr0. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra