proposition: Lemma is_even_0: is_even 0 = true.
proof: Proof. apply refl_equal. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance