proposition: Lemma gcd_mod : forall a b, b~=0 -> gcd (a mod b) b == gcd b a.
proof: Proof. intros a b Hb. rewrite mod_eq; trivial. rewrite <- add_opp_r, mul_comm, <- mul_opp_l. rewrite (gcd_comm _ b). apply gcd_add_mult_diag_r. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor