proposition: Lemma even_double : forall n, Nat.Even_alt (Nat.double n).
proof: Proof. intro n; unfold Nat.double; replace (n + n) with (2*n); [apply Nat.Even_alt_Even; exists n; reflexivity | lia]. Defined.
imports: Coq(ZArith) Coq(Lia)