proposition: Lemma Odd_div2 : forall n : nat, Nat.Odd n -> S (Nat.div2 n) = Nat.div2 (S n).
proof: Proof. intros n [k ->]; rewrite Nat.add_1_r, Nat.div2_succ_double. rewrite <-(Nat.add_1_r (S (2 * k))), (Nat.add_succ_comm (2 * k)). rewrite <-(Nat.mul_1_r 2) at 2. rewrite <-(Nat.mul_add_distr_l 2), Nat.add_succ_r. now rewrite Nat.add_0_r, Nat.div2_double. Qed.
imports: Coq.Arith(PeanoNat)