proposition: Theorem Zrem_Zmod_pos : forall a b, 0 <= a -> 0 < b -> Z.rem a b = a mod b.
proof: Proof. intros a b Ha Hb; generalize (Zquotrem_Zdiv_eucl_pos a b Ha Hb); intuition. Qed.
imports: Nnat ZArith_base Lia ZArithRing Zdiv Morphisms