proposition: Lemma odd_add_odd_inv_r n m : Nat.Odd (n + m) -> Nat.Even n -> Nat.Odd m.
proof: Proof. destruct m as [|m]. rewrite Nat.add_0_r; intros; case (Nat.Even_Odd_False n); auto. intros [x Hmn] [y Hn]; exists (x - y). rewrite Nat.mul_sub_distr_l, <- Nat.sub_succ. rewrite <- (Nat.add_1_r (2 * x)), <- Hmn, <- Hn. rewrite <- (Nat.add_succ_comm n), (Nat.add_comm (S n)). rewrite Nat.add_sub, Nat.add_1_r; auto. Qed.
imports: Coq(Div2 Even Wf_nat Arith ArithRing List) Bertrand(Bertrand)