proposition: Theorem Zquotrem_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b -> a÷b = a/b /\ Z.rem a b = a mod b.
proof: Proof. intros. apply Zdiv_mod_unique with b. - apply Zrem_lt_pos; lia. - rewrite Z.abs_eq by lia. apply Z_mod_lt; lia. - rewrite <- Z_div_mod_eq_full. symmetry; apply Z.quot_rem; lia. Qed.
imports: Nnat ZArith_base Lia ZArithRing Zdiv Morphisms