proposition: Lemma bits_inj_0 : forall a, (forall n, a.[n] = false) -> a == 0.
proof: Proof. intros a H. destruct (eq_decidable a 0) as [EQ|NEQ]; trivial. apply bit_log2 in NEQ. now rewrite H in NEQ. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog