proposition: Lemma even_or_odd : forall n : nat, exists k, n = 2 * k \/ n = S (2 * k).
proof: Proof. induction n. exists 0. now left. destruct IHn as [k [Hk|Hk]]. exists k. right. now apply f_equal. exists (S k). left. lia. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)