proposition: Lemma hqplusr0 ( x : hq ) : paths ( x + 0 ) x .
proof: Proof. Proof . apply ( ringrunax1 _ x ) . Defined . Lemma hqplusl0 ( x : hq ) : paths ( 0 + x ) x . Proof . apply ( ringlunax1 _ x ) . Defined . Lemma hqplusassoc ( x y z : hq ) : paths ( ( x + y ) + z ) ( x + ( y + z ) ) . Proof . intros . apply ( ringassoc1 hq x y z ) . Defined . Lemma hqpluscomm ( x y : hq ) : paths ( x + y ) ( y + x ) . Proof . intros . apply ( ringcomm1 hq x y ) . Defined . Lemma hqlminus ( x : hq ) : paths ( -x + x ) 0 . Proof . apply ( ringlinvax1 hq x ) . Defined . Lemma hqrminus ( x : hq ) : paths ( x - x ) 0 . Proof . apply ( ringrinvax1 hq x ) . Defined . Lemma isinclhqplusr ( n : hq ) : isincl ( λ m : hq, m + n ) . Proof. apply ( pr2 ( weqtoincl ( weqrmultingr hqaddabgr n ) ) ) . Defined.
imports: UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.NumberSystems.Integers 