proposition: Theorem mask_def: forall k m n, is_mask m n -> forall p, testbit (mask k m) p = if le_gt_dec n p then false else testbit k p.
proof: Proof. intros k m n P. intros. apply mask_spec with (k:=k) in P. destruct P as (P1 & P2). destruct (le_gt_dec n p). apply P2. lia. apply P1. lia. Qed.
imports: List Bool ZArith Lia