(* ---------------------------------------------------------- *) (* --- Preservation of Invariant (file remainder.c, line 8) --- *) (* ---------------------------------------------------------- *) Require Import ZArith. Require Import Reals. Require Import BuiltIn. Require Import int.Int. Require Import int.Abs. Require Import int.ComputerDivision. Require Import real.Real. Require Import real.RealInfix. Require Import real.FromInt. Require Import map.Map. Require Import Qedlib. Require Import Qed. Require Import bool.Bool. Require Import Zbits. Require Import Cint. Goal forall (i_2 i_1 i : Z), let x := (i%Z - i_1%Z)%Z in let x_1 := (i%Z + (i_2 * x)%Z)%Z in ((0 <= i)%Z) -> ((0 <= i_1)%Z) -> ((i_1 < i)%Z) -> ((0 <= x_1)%Z) -> ((is_sint32 i%Z)) -> ((is_sint32 i_1%Z)) -> ((is_sint32 x)) -> ((is_sint32 x_1)) -> (exists i_3 : Z, ((i_1 + (i_3 * x)) = x_1)%Z). Proof. intros q b r. intros. exists (q+1). unfold x_1. unfold x. ring. Qed.