proposition: Theorem div2_plus_2 : forall n k, div2 (n + 2 * k) = div2 n + k.
proof: Proof. induction n; intros. simpl. rewrite Nat.add_0_r. replace (k + k) with (2 * k) by lia. apply div2_double. replace (S n + 2 * k) with (S (n + 2 * k)) by lia. destruct (Even_Odd_dec n). - rewrite <- Even_div2. rewrite <- Even_div2 by auto. apply IHn. apply Even_Even_add; auto. apply Even_mul_l. now exists 1. - rewrite <- Odd_div2. rewrite <- Odd_div2 by auto. rewrite IHn. lia. apply Odd_add_l; auto. now exists k. Qed.
imports: Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Bool.Bool Coq.Arith.Arith Coq.micromega.Lia Coq.NArith.NArith Coq.ZArith.ZArith bbv.N_Z_nat_conversions bbv.Nomega