proposition: Lemma Zmod_small : forall m a : Z, (m > 0)%Z -> (0 <= a < m)%Z -> (a mod m)%Z = a.
proof: Proof. intros m a Hm Ha. apply (Zmodeq_small (a mod m) a m). apply (Z_mod_lt a m Hm). exact Ha. replace (a mod m - a)%Z with (- m * (a / 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 H; rewrite H. 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