proposition: Lemma bits_inj : forall a b, testbit a === testbit b -> a == b.
proof: Proof. intros a. pattern a. apply strong_right_induction with 0;[clear a|apply le_0_l]. intros a _ IH b H. destruct (eq_0_gt_0_cases a) as [EQ|LT]. - rewrite EQ in H |- *. symmetry. apply bits_inj_0. intros n. now rewrite <- H, bits_0. - rewrite (div_mod a 2), (div_mod b 2) by order'. f_equiv; [ | now rewrite <- 2 bit0_mod, H]. f_equiv. apply IH; trivial using le_0_l. + apply div_lt; order'. + intro n. rewrite 2 div2_bits. apply H. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog