proposition: Lemma even_or_odd_plus_gt : forall i j : nat, i <= j -> {k : nat & {j = i + (k + k)} + {j = i + S (k + k)}}.
proof: Proof. intros i j H. destruct (even_or_odd_plus (j - i)) as [k [Hk | Hk]]; exists k. destruct (Nat.eq_dec k 0) as [-> | I]. - left; rewrite Nat.add_0_r; rewrite Nat.add_0_r in Hk. now apply Nat.sub_0_le in Hk; apply Nat.le_antisymm. - left; apply Nat.add_sub_eq_nz in Hk; [| now intros [C _]%Nat.eq_add_0]. exact (eq_sym Hk). - right; apply Nat.add_sub_eq_nz in Hk; [| now intros C]. exact (eq_sym Hk). Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)