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