proposition: Lemma div2_le_n : forall n, Nat.div2 n <= n.
proof: Proof. cut (forall n, Nat.div2 n <= n /\ Nat.div2 (S n) <= S n). intros H n; gen (H n); tauto. induction n; auto. inversion IHn; split; auto. simpl. apply le_n_S. auto with arith. Qed.
imports: Coq(Lia PeanoNat) CoLoR(LogicUtil NatCompat)