proposition: Lemma bits_0 : forall n, 0.[n] = false.
proof: Proof. intros n. destruct (le_gt_cases 0 n). - apply testbit_false; trivial. nzsimpl; order_nz. - now apply testbit_neg_r. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog