Lemma hzgcdsymm ( m n : hz ) : hzgcd m n = hzgcd n m. Proof. intros. assert ( make_hProp ( hzgcd m n ) ( isaprophzgcd _ _ ) = ( make_hProp ( hzgcd n m ) ( isaprophzgcd _ _ ) ) ) as x. { apply hPropUnivalence. - intro i. destruct i as [ a i ]. destruct i as [ i0 i1 ]. destruct i0 as [ j0 j1 ]. split with a. split. + split; assumption. + intros l o. apply i1. split. * exact ( pr2 o ). * exact ( pr1 o ). - intro i. destruct i as [ a i ]. destruct i as [ i0 i1 ]. destruct i0 as [ j0 j1 ]. split with a. split. + split; assumption. + intros l o. apply i1. split. * exact ( pr2 o ). * exact ( pr1 o ). } apply ( base_paths _ _ x ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.