proposition: Lemma Remainder_equiv : forall r b, Remainder r b <-> Remainder_alt r b.
proof: Proof. unfold Remainder, Remainder_alt. intros [ | r | r ] [ | b | b ]; intuition try easy. - now apply Z.opp_lt_mono. - right; split. + now apply Z.opp_lt_mono. + apply Pos2Z.neg_is_nonpos. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms