proposition: Theorem mask_spec': forall k m n, is_mask m n -> mask (mask k m) m = mask k m.
proof: Proof. intros. apply testbit_spec; intros. rewrite !mask_def with (n:=n);auto. destruct (le_gt_dec n n0);auto. Qed.
imports: List Bool ZArith Lia