proposition: Theorem zerobit_spec: forall k m n, is_mask m n -> zerobit k m = negb (testbit k n).
proof: Proof. intros k m n P. unfold zerobit; simpl. apply eq_bool_prop_intro. rewrite !Is_true_true. rewrite eqb_spec. assert (MD := is_mask_def _ _ P). split ; intro. - apply (f_equal (fun x => testbit x n)) in H. rewrite zero_spec in H. rewrite land_spec in H. rewrite MD in H. destruct (Nat.eq_dec n n); try congruence. rewrite andb_true_r in H. rewrite H. reflexivity. - apply testbit_spec. intro p. rewrite land_spec. rewrite zero_spec. rewrite negb_true_iff in H. rewrite MD. destruct (Nat.eq_dec p n). { subst. rewrite H. reflexivity. } { rewrite andb_false_r. reflexivity. } Qed.
imports: List Bool ZArith Lia