proposition: Lemma even_spec n : even n = true <-> Even n.
proof: Proof. split. - exists (div2 n). now destruct n as [|[ | | ]|[ | | ]]. - intros (m,->). now destruct m. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass