proposition: Lemma nat_double_or_s_double : forall n, {exists p, n = double p} + {exists p, n = S (double p)}.
proof: Proof. induction n as [| n IHn]. - left; exists 0; auto with arith. - induction IHn as [a | b]. + right; destruct a as [x H]; exists x; now rewrite H. + left; destruct b as [x H]; exists (S x). rewrite H; symmetry. cbn; unfold double; lia. Qed.
imports: Coq(Arith Lia )