proposition: Lemma ones_spec_iff : forall n m, (ones n).[m] = true <-> m<n.
proof: Proof. intros. split. - intros H. apply lt_nge. intro H'. apply ones_spec_high in H'. rewrite H in H'; discriminate. - apply ones_spec_low. Qed.
imports: Bool NAxioms NSub NPow NDiv NParity NLog