proposition: Lemma bits_inj : forall a b, testbit a === testbit b -> a == b.
proof: Proof. assert (AUX : forall n, 0<=n -> forall a b, 0<=a<2^n -> testbit a === testbit b -> a == b). { intros n Hn. apply le_ind with (4:=Hn). - solve_proper. - intros a b Ha H. rewrite pow_0_r, one_succ, lt_succ_r in Ha. assert (Ha' : a == 0) by (destruct Ha; order). rewrite Ha' in *. symmetry. apply bits_inj_0. intros m. now rewrite <- H, bits_0. - clear n Hn. intros n Hn IH a b (Ha,Ha') H. rewrite (div_mod a 2), (div_mod b 2) by order'. f_equiv; [ | now rewrite <- 2 bit0_mod, H]. f_equiv. apply IH. + split. * apply div_pos; order'. * apply div_lt_upper_bound. { order'. } now rewrite <- pow_succ_r. + intros m. destruct (le_gt_cases 0 m). * rewrite 2 div2_bits by trivial. apply H. * now rewrite 2 testbit_neg_r. } intros a b H. destruct (le_gt_cases 0 a) as [Ha|Ha]. - apply (AUX a); trivial. split; trivial. apply pow_gt_lin_r; order'. - apply succ_inj, opp_inj. assert (0 <= - S a). { apply opp_le_mono. now rewrite opp_involutive, opp_0, le_succ_l. } apply (AUX (-(S a))); trivial. + split; trivial. apply pow_gt_lin_r; order'. + intros m. destruct (le_gt_cases 0 m). * now rewrite 2 bits_opp, 2 pred_succ, H. * now rewrite 2 testbit_neg_r. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog