proposition: Theorem mask_spec': forall k m n, is_mask m n -> mask (mask k m) m = mask k m.
proof: Proof. intros. generalize (mask_spec k m n H). intros [HA HB]. generalize (mask_spec (mask k m) m n H). intros [HC HD]. eapply testbit_spec; intros. unfold testbit in *. destruct (lt_dec n0 n). - apply HC; auto. - rewrite HB; try lia; auto. apply HD; lia. Qed.
imports: Lia Cdcl.Coqlib