proposition: Lemma Zmodeq_gcd_compat_lft : forall a b : Z, Zmodeq a b -> Zgcd m a = Zgcd m b.
proof: Proof. unfold Zmodeq in |- *. intros a b H0. elim H0; intros q Hq. replace (Zgcd m b) with (Zgcd m (b + q * m)); auto with zarith. rewrite Hq. replace (b + (a - b))%Z with a; auto with zarith. Qed.
imports: CoRN.model.Zmod.ZGcd