(* This file is generated by Why3's Coq 8.4 driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require Import ZOdiv. Require BuiltIn. Require int.Int. Require int.Abs. Require int.ComputerDivision. Axiom mod_div_unique : forall (x:Z) (y:Z) (q:Z) (r:Z), ((0%Z <= x)%Z /\ ((0%Z < y)%Z /\ ((x = ((q * y)%Z + r)%Z) /\ ((0%Z <= r)%Z /\ (r < y)%Z)))) -> ((q = (ZOdiv x y)) /\ (r = (ZOmod x y))). Open Scope Z_scope. (* Why3 goal *) Theorem mod_succ_1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> ((~ ((ZOmod (x + 1%Z)%Z y) = 0%Z)) -> ((ZOmod (x + 1%Z)%Z y) = ((ZOmod x y) + 1%Z)%Z)). (* Why3 intros x y (h1,h2) h3. *) intros x y (Hx,Hy) H. assert (h: y>0) by omega. generalize (ZO_div_mod_eq x y); intro h1. generalize (ZO_div_mod_eq (x+1) y); intro h2. assert (h3:x = y * (ZOdiv (x + 1) y) + (ZOmod (x + 1) y - 1)) by omega. generalize (mod_div_unique x y (ZOdiv (x + 1) y) (ZOmod (x + 1) y - 1)). intuition. destruct H1 ; auto with zarith. rewrite h3 at 1. ring. assert (0 <= ZOmod (x + 1) y < y). apply Zquot.Zrem_lt_pos_pos; omega. omega. Qed.