proposition: Lemma Remainder_equiv : forall a b r, Remainder a b r <-> Remainder_alt a b r.
proof: Proof. unfold Remainder, Remainder_alt; intuition auto with zarith. - lia. - lia. - rewrite <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; lia. - assert (0 <= Z.sgn r * Z.sgn a). { rewrite <-Z.sgn_mul, Z.sgn_nonneg; auto. } destruct r; simpl Z.sgn in *; lia. Qed.
imports: Nnat ZArith_base Lia ZArithRing Zdiv Morphisms