proposition: Lemma x_gt_Zdiv2 : forall x : Z, Zeven.Zeven x -> (x > 0)%Z -> (x > Zeven.Zdiv2 x)%Z.
proof: Proof. simple destruct x. simpl in |- *. auto. simpl in |- *. simple destruct p. intuition. simpl in |- *. intros. rewrite BinInt.Zpos_xO. generalize H0. rewrite BinInt.Zpos_xO. intro. omega. auto. discriminate. Qed.
imports: ZArith Omega