proposition: Lemma bits_inj' : forall a b, (forall n, 0<=n -> a.[n] = b.[n]) -> a == b.
proof: Proof. intros a b H. apply bits_inj. intros n. destruct (le_gt_cases 0 n). - now apply H. - now rewrite 2 testbit_neg_r. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog