proposition: Lemma hzgcdandminusl ( m n : hz ) : hzgcd m n = hzgcd ( - m ) n.
proof: Proof. intros. assert ( make_hProp ( hzgcd m n ) ( isaprophzgcd _ _ ) = ( make_hProp ( hzgcd ( - m ) n ) ( 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. * use (hinhuniv _ j0). intro k. destruct k as [ k f ]. unfold hzdiv0 in f. intros P s. apply s. split with ( - k ). unfold hzdiv0. rewrite ( ringrmultminus hz ). apply maponpaths. assumption. * assumption. + intros l f. apply i1. split. * use (hinhuniv _ ( pr1 f )). intro k. destruct k as [ k g ]. unfold hzdiv0 in g. intros P s. apply s. split with ( - k ). unfold hzdiv0. rewrite ( ringrmultminus hz ). rewrite <- ( ringminusminus hz m). apply maponpaths. assumption. * exact ( pr2 f ). - intro i. destruct i as [ a i ]. destruct i as [ i0 i1 ]. destruct i0 as [ j0 j1 ]. split with a. split. + split. * use (hinhuniv _ j0). intro k. destruct k as [ k f ]. unfold hzdiv0 in f. intros P s. apply s. split with ( - k ). unfold hzdiv0. rewrite ( ringrmultminus hz ). rewrite <- ( ringminusminus hz m ). apply maponpaths. assumption. * assumption. + intros l f. apply i1. split. * use (hinhuniv _ ( pr1 f )). intro k. destruct k as [ k g ]. unfold hzdiv0 in g. intros P s. apply s. split with ( - k ). unfold hzdiv0. rewrite (ringrmultminus hz ). apply maponpaths. assumption. * exact ( pr2 f ). } apply ( base_paths _ _ x ). Defined.
imports: UniMath.PAdics.lemmas UniMath.NumberSystems.Integers UniMath.Foundations.Preamble