proposition: Lemma ones_spec_iff : forall n m, 0<=n -> ((ones n).[m] = true <-> 0<=m<n).
proof: Proof. intros n m Hn. split. - intros H. destruct (lt_ge_cases m 0) as [Hm|Hm]. + now rewrite testbit_neg_r in H. + split; trivial. apply lt_nge. intro H'. rewrite ones_spec_high in H. * discriminate. * now split. - apply ones_spec_low. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog