proposition: Lemma div2_lt : forall n, n <> 0 -> div2 n < n.
proof: Proof. induction n as [| | n IHn] using div2_rect; auto. - now destruct 1. - simpl;intros. apply Nat.le_lt_trans with (S n);auto. generalize (div2_le n);auto with arith. Qed.
imports: Arith ArithRing Lia Recdef