proposition: Lemma odd_add_even_inv_r n m : Nat.Odd (n + m) -> Nat.Odd n -> Nat.Even m.
proof: Proof. intros [x Hmn] [y Hn]; exists (x - y). rewrite Nat.mul_sub_distr_l, <- Nat.sub_succ. rewrite <- Nat.add_1_r, <- Hmn, <- Nat.add_1_r, <- Hn. rewrite Nat.add_comm, Nat.add_sub; auto. Qed.
imports: Coq(Div2 Even Wf_nat Arith ArithRing List) Bertrand(Bertrand)