Require Import Arith.

(* Theorem about addition (Plus) *)
Theorem OddOddEvenP: forall n m:nat,
  Nat.Odd n -> Nat.Odd m -> Nat.Even (n+m).
Proof.
  intros n m Hp Hq.
  destruct Hp as [p Hp].
  destruct Hq as [q Hq].
  unfold Nat.Even.
  exists (p+q+1).
  rewrite Nat.mul_add_distr_l.
  rewrite Nat.mul_add_distr_l.
  rewrite Nat.mul_1_r.
  rewrite Hp.
  rewrite Hq.
  ring.
Qed.

Theorem OddEvenOddP: forall n m:nat,
  Nat.Odd n -> Nat.Even m -> Nat.Odd (n+m).
Proof.
  intros n m [p Hp] [q Hq].
  unfold Nat.Odd.
  exists (p+q).
  rewrite Nat.mul_add_distr_l.
  rewrite Hp.
  rewrite Hq.
  ring.
Qed.

Theorem EvenEvenEvenP: forall n m:nat,
  Nat.Even n -> Nat.Even m -> Nat.Even (n+m).
Proof.
  intros n m [p Hp] [q Hq].
  unfold Nat.Even.
  exists (p+q).
  rewrite Nat.mul_add_distr_l.
  rewrite Hp.
  rewrite Hq.
  ring.
Qed.


(* Theorem about subtraction (Minus) *)
Theorem OddOddEvenM: forall n m:nat,
  Nat.Odd n -> Nat.Odd m -> Nat.Even (n-m).
Proof.
  intros n m [p Hp] [q Hq].
  unfold Nat.Even.
  exists (p-q).
  rewrite Nat.mul_sub_distr_l.
  rewrite Hp.
  rewrite Hq.
  (* doing [lia] here would solve this goal *)
  simpl.
  rewrite Nat.add_0_r.
  rewrite Nat.add_0_r.
  rewrite (Nat.add_comm (q+q) 1).
  replace (p + p + 1) with (1 + p + p) by ring.
  Print Nat.sub.
  simpl.
  reflexivity.
Qed.

Theorem EvenEvenEvenM: forall n m:nat,
  Nat.Even n -> Nat.Even m -> Nat.Even (n-m).
Proof.
  intros n m [p Hp] [q Hq].
  unfold Nat.Even.
  exists (p-q).
  rewrite Hp.
  rewrite Hq.
  rewrite Nat.mul_sub_distr_l.
  reflexivity.
Qed.

Require Import Lia.
(* 1-2 is 0 but is even. So m<=n constraint has to be there *)
Theorem OddEvenOddM: forall n m:nat,
  Nat.Odd n -> Nat.Even m -> m<=n -> Nat.Odd (n-m).
Proof.
  intros n m [p Hp] [q Hq] H.
  unfold Nat.Odd.
  exists (p-q).
  rewrite Hp.
  rewrite Hq.
  rewrite Nat.mul_sub_distr_l.
  replace (2*p+1) with (1+2*p) by ring.
  rewrite (Nat.add_comm (2*p-2*q) 1).
  SearchRewrite (_ + (_ - _)).
  rewrite Nat.add_sub_assoc.
  - reflexivity.
  - lia.

Restart.
  (* Another way *)
  (* https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/lia.20shows.20error.2E *)
  (* Thanks to Pierre Castéran *)
  intros n m [p Hp] [q Hq] H.
  subst.
  exists (p-q).
  lia.
Qed.