proposition: Lemma rem_divide : forall a b, b~=0 -> (a rem b == 0 <-> (b|a)).
proof: Proof. intros a b Hb. split. - intros Hab. exists (a÷b). rewrite mul_comm. rewrite (quot_rem a b Hb) at 1. rewrite Hab; now nzsimpl. - intros (c,Hc). rewrite Hc. now apply rem_mul. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor