proposition: Lemma div_mod_eq x y : x = y*(x/y) + x mod y.
proof: Proof. destruct y as [|y]; [reflexivity | ]. unfold div, modulo. generalize (divmod_spec x y 0 y (le_n y)). destruct divmod as (q,u). intros (U,V). simpl in *. now rewrite mul_0_r, sub_diag, !add_0_r in U. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass