proposition: Lemma testbit_unique : forall a n (a0:bool) l h, l<2^n -> a == l + (a0 + 2*h)*2^n -> a.[n] = a0.
proof: Proof. intros a n a0 l h Hl EQ. apply b2n_inj. rewrite testbit_spec' by trivial. symmetry. apply mod_unique with h. - destruct a0; simpl; order'. - symmetry. apply div_unique with l; trivial. now rewrite add_comm, (add_comm _ a0), mul_comm. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog