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 -{2}(Nat.mul_1_r 2) -(Nat.mul_add_distr_l 2) Nat.add_succ_r. now rewrite Nat.add_0_r Nat.div2_double. Qed.
imports: Coq(Reals Psatz ssreflect)