proposition: Lemma div2_decr a n : a <= S n -> div2 a <= n.
proof: Proof. destruct a as [|a]; intros H. - simpl; apply le_0_l. - apply succ_le_mono in H. apply le_trans with a; [ apply le_div2 | trivial ]. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass