Lemma hqgthgehtrans ( n m k : hq ) : hqgth n m -> hqgeh m k -> hqgth n k . Proof. intros gnm gmk . destruct ( hqgehchoice m k gmk ) as [ g' | e ] . apply ( istranshqgth _ _ _ gnm g' ) . rewrite e in gnm . apply gnm . Defined.
Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.