proposition: Lemma mod_bound_pos x y : 0<=x -> 0<y -> 0 <= x mod y < y.
proof: Proof. intros Hx Hy. split. - apply le_0_l. - destruct y; [ now elim Hy | clear Hy ]. unfold modulo. apply lt_succ_r, le_sub_l. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass