proposition: Lemma mask_big : forall m n (BOUND : n >= 63) (BITN : is_mask m n), False.
proof: Proof. unfold is_mask. intros. generalize (BITN n). generalize (BITN (n+1)). intros. unfold testbit in *. replace (63 <=? n +1) with true in * by lia. replace ( 63 <=? n) with true in * by lia. intuition lia. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR