proposition: Lemma even_spec n : even n = true <-> Even n.
proof: Proof. destruct n as [|p]. - split. + now exists 0. + trivial. - destruct p as [p|p|]; simpl; split; try easy. + intros (m,H). now destruct m. + now exists (pos p). + intros (m,H). now destruct m. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties