proposition: Theorem ZOdiv_small_abs : forall a b, (Z.abs a < b)%Z -> Z.quot a b = Z0.
proof: Proof. intros a b Ha. destruct (Zle_or_lt 0 a) as [H|H]. apply Z.quot_small. split. exact H. now rewrite Z.abs_eq in Ha. apply Z.opp_inj. rewrite <- Zquot_opp_l, Z.opp_0. apply Z.quot_small. generalize (Zabs_non_eq a). lia. Qed.
imports: Coq(ZArith Lia Zquot)