proposition: Lemma div_mul : forall a b, b~=0 -> (a*b)/b == a.
proof: Proof. intros a b ?. symmetry. apply div_unique with 0. - destruct (lt_ge_cases 0 b); [left|right]; split; order. - nzsimpl; apply mul_comm. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZDiv