proposition: Lemma quot_div_nonneg : forall a b, 0<=a -> 0<b -> a÷b == a/b.
proof: Proof. intros a b **. apply div_unique_pos with (a rem b). - now apply rem_bound_pos. - apply quot_rem. order. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor