proposition: Lemma Zmod_opp_elim : forall m a : Z, (m > 0)%Z -> (- a mod m)%Z = ((m - a mod m) mod m)%Z.
proof: Proof. intros m a Hm. apply Zmod_minus_intro. exact Hm. replace (- a - (m - a mod m))%Z with (- m + (a mod m - a))%Z; auto with zarith. replace (- m)%Z with (-1 * m)%Z; auto with zarith. rewrite Zmod_cancel_multiple; auto. replace (a mod m - a)%Z with (- (a / m) * m)%Z; auto with zarith. generalize (Z_div_mod_eq_full a m). set (q := (a / m)%Z); set (r := (a mod m)%Z); intro Ha; rewrite Ha. rewrite Zplus_comm; unfold Zminus in |- *; rewrite Zopp_plus_distr; rewrite Zplus_assoc; rewrite Zplus_opp_r; rewrite Zplus_0_l; rewrite Zopp_mult_distr_l_reverse; rewrite Zmult_comm; reflexivity. Qed.
imports: CoRN.model.Zmod.ZGcd