proposition: Theorem mod_bound_pos a b : 0<=a -> 0<b -> 0 <= a mod b < b.
proof: Proof. intros _ H. split. - apply le_0_l. - apply mod_lt. now destruct b. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties