proposition: Lemma mod_divides : forall a b, b~=0 -> (a mod b == 0 <-> (b|a)).
proof: Proof. intros a b Hb. split. - intros Hab. exists (a/b). rewrite mul_comm. rewrite (div_mod a b Hb) at 1. rewrite Hab; now nzsimpl. - intros (c,Hc). rewrite Hc. now apply mod_mul. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv