proposition: Lemma exponent_div2_floor_correct : forall e, let (e',b) := exponent_div2_floor e in EtoZ e = (2 * EtoZ e' + if b then 1 else 0)%Z.
proof: Proof. unfold EtoZ, exponent_div2_floor. intros [|[e|e|]|[e|e|]] ; try easy. rewrite <- Pos.add_1_r. change (- (2 * Zpos e + 1) = 2 * - (Zpos e + 1) + 1)%Z. ring. Qed.
imports: Coq(ZArith Reals Psatz Bool) Flocq(Zaux Raux) Basic Generic Generic_proof Specific_sig