proposition: Theorem Zquot_Zdiv_pos : forall a b, 0 <= a -> 0 <= b -> a÷b = a/b.
proof: Proof. intros a b Ha Hb. Z.le_elim Hb. - generalize (Zquotrem_Zdiv_eucl_pos a b Ha Hb); intuition. - subst; now rewrite Zquot_0_r, Zdiv_0_r. Qed.
imports: Nnat ZArith_base Lia ZArithRing Zdiv Morphisms