proposition: Lemma adjust_pos_correct : forall q r pos, (1 < Zpos q)%Z -> (0 <= r < Zpos q)%Z -> convert_location_inv (adjust_pos r q pos) = new_location (Zpos q) r (convert_location_inv pos).
proof: Proof. unfold adjust_pos, new_location, new_location_even, new_location_odd. intros [q|q|] r pos Hq (Hr1, Hr2). destruct r as [|r|r] ; simpl. now case pos. change (r~1 ?= q~1)%positive with (r ?= q)%positive. now case ((r ?= q)%positive) ; case pos ; simpl. unfold Zeven. now elim Hr1. destruct r as [|r|r] ; simpl. now case pos. change (r~0 ?= q~0)%positive with (r ?= q)%positive. now case ((r ?= q)%positive) ; case pos. now elim Hr1. discriminate Hq. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic