Div2.v 1.13 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12 13 14 15 16
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
17

18 19 20 21 22 23 24 25 26 27 28 29 30 31
Require Import int.EuclideanDivision.

(* Why3 goal *)
Lemma div2 : forall (x:Z), exists y:Z, (x = (2%Z * y)%Z) \/
  (x = ((2%Z * y)%Z + 1%Z)%Z).
Proof.
intros x.
exists (div x 2).
refine (_ (Mod_bound x 2 _) (Div_mod x 2 _)) ; try easy.
intros H1 H2.
simpl in H1.
omega.
Qed.