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