proposition: Lemma even_double n : Nat.Even n -> n = Nat.double (Nat.div2 n).
proof: Proof. intros [x ->]; rewrite Nat.div2_double; unfold Nat.double; ring. Qed.
imports: Coq(Div2 Even Wf_nat Arith ArithRing List) Bertrand(Bertrand)