proposition: Lemma nat_comp : forall(a : nat), exists x : nat, (a = (2 * x) \/ a = (S (2 * x))).
proof: Proof. induction a. exists 0. simpl. auto. elim IHa. clear IHa. intros. destruct H. subst. simpl. exists x. right. auto. subst. simpl. exists (S x). left. simpl. lia. Qed.
imports: ZArith micromega.Lia