proposition: Lemma Z_mod_remainder a b : b<>0 -> Remainder (a mod b) b.
proof: Proof. unfold Z.modulo; intros Hb; generalize (Z_div_mod_full a b Hb); auto. destruct Z.div_eucl; tauto. Qed.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms