proposition: Lemma Zdiv2_positive : forall x : Z, Zeven.Zeven x -> (x >= 0)%Z -> (Zeven.Zdiv2 x >= 0)%Z.
proof: Proof. simple destruct x. simpl in |- *. omega. simpl in |- *. simple destruct p. intuition. simpl in |- *. intros. auto. intuition. simpl in |- *. simple destruct p. intuition. simpl in |- *. intuition. intuition. Qed.
imports: ZArith Omega