proposition: Lemma hqgehgthtrans ( n m k : hq ) : hqgeh n m -> hqgth m k -> hqgth n k .
proof: Proof. intros gnm gmk . destruct ( hqgehchoice n m gnm ) as [ g' | e ] . apply ( istranshqgth _ _ _ g' gmk ) . rewrite e . apply gmk . Defined.
imports: UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.NumberSystems.Integers 