proposition: Theorem mod_bound_pos_le a b : 0 <= a -> 0 < b -> 0 <= a mod b <= a.
proof: Proof. now intros; split; [apply Z.mod_bound_pos | apply Z.mod_le]. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass