proposition: Theorem Zrem_sgn a b : 0 <= Z.sgn (Z.rem a b) * Z.sgn a.
proof: Proof. zero_or_not b. - zero_or_not (Z.rem a b). rewrite Z.rem_sign_nz; trivial. apply Z.square_nonneg. Qed.
imports: Nnat ZArith_base Lia ZArithRing Zdiv Morphisms