examples/euler001/euler001_DivModHints_mod_div_unique_1.v

   1 (* This file is generated by Why3's Coq driver *)
   2 (* Beware! Only edit allowed sections below    *)
   3 Require Import BuiltIn.
   4 Require BuiltIn.
   5 Require int.Int.
   6 Require int.Abs.
   7 Require int.ComputerDivision.
   8
   9 (* Why3 goal *)
  10 Theorem mod_div_unique'vc :
  11   forall (x:Numbers.BinNums.Z) (y:Numbers.BinNums.Z) (q:Numbers.BinNums.Z)
  12     (r:Numbers.BinNums.Z),
  13   (0%Z <= x)%Z /\
  14   (0%Z < y)%Z /\ (x = ((q * y)%Z + r)%Z) /\ (0%Z <= r)%Z /\ (r < y)%Z ->
  15   (q = (ZArith.BinInt.Z.quot x y)) /\ (r = (ZArith.BinInt.Z.rem x y)).
  16 Proof.
  17 intros x y q r (h1,(h2,(h3,(h4,h5)))).
  18 apply Zquot.Zquot_mod_unique_full.
  19 2: rewrite h3; ring.
  20 red.
  21 left.
  22 rewrite Z.abs_eq; auto with zarith.
  23 Qed.
  24