proposition: Lemma bits_inj_0 : forall a, (forall n, a.[n] = false) -> a == 0.
proof: Proof. intros a H. destruct (lt_trichotomy a 0) as [Ha|[Ha|Ha]]; trivial. - apply (bits_above_log2_neg a (S (log2 (P (-a))))) in Ha. + now rewrite H in Ha. + apply lt_succ_diag_r. - apply bit_log2 in Ha. now rewrite H in Ha. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog