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 exponent_div2_floor. intros [e|e]. unfold EtoZ. simpl BigZ.to_Z. rewrite BigN.spec_shiftr. rewrite <- Z.div2_spec. rewrite BigN.spec_even. rewrite <- Zodd_even_bool. apply Zdiv2_odd_eqn. rewrite BigN.spec_even. case_eq (Z.even (BigN.to_Z e)). unfold EtoZ. simpl BigZ.to_Z. rewrite BigN.spec_shiftr. rewrite <- Z.div2_spec. rewrite (Zdiv2_odd_eqn (BigN.to_Z e)) at 2. rewrite Zodd_even_bool. intros ->. simpl negb ; cbv iota. ring. unfold EtoZ. simpl BigZ.to_Z. rewrite BigN.spec_succ. rewrite BigN.spec_shiftr. rewrite <- Z.div2_spec. rewrite (Zdiv2_odd_eqn (BigN.to_Z e)) at 2. rewrite Zodd_even_bool. intros ->. simpl negb ; cbv iota. ring. Qed.
imports: Coq(Bool ZArith Reals Psatz) Bignums(BigN BigZ) Flocq(Zaux Raux Digits) Basic Generic Generic_proof Specific_sig