proposition: Lemma le_div2 n : div2 (S n) <= n.
proof: Proof. revert n. fix le_div2 1. intro n; destruct n as [|n]; simpl; trivial. apply lt_succ_r. destruct n; [simpl|]; trivial. now constructor. Qed.
imports: NAxioms NProperties OrdersFacts DecidableClass