Lemma isinclhqplusr ( n : hq ) : isincl ( λ m : hq, m + n ) . Proof. apply ( pr2 ( weqtoincl ( weqrmultingr hqaddabgr n ) ) ) . Defined.
Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.