proposition: Lemma testbit_unique : forall a n (a0:bool) l h, 0<=l<2^n -> a == l + (a0 + 2*h)*2^n -> a.[n] = a0.
proof: Proof. intros a n a0 l h Hl EQ. assert (0<=n). { destruct (le_gt_cases 0 n) as [Hn|Hn]; trivial. rewrite pow_neg_r in Hl by trivial. destruct Hl; order. } apply b2z_inj. rewrite testbit_spec' by trivial. symmetry. apply mod_unique with h. - left; destruct a0; simpl; split; order'. - symmetry. apply div_unique with l. + now left. + now rewrite add_comm, (add_comm _ a0), mul_comm. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog