proposition: Lemma Even_Odd_False : forall x, Even x -> Odd x -> False.
proof: Proof. intros x (y,E) (z,O). rewrite O in E; clear O. destruct (le_gt_cases y z) as [LE|GT]. - generalize (double_below _ _ LE); order. - generalize (double_above _ _ GT); order. Qed.
imports: Bool NZAxioms NZMulOrder