proposition: Theorem match_prefix_spec: forall k p m n, is_mask m n -> mask p m = p -> (match_prefix k p m = true <-> forall q, (q < n)%nat -> testbit k q = testbit p q).
proof: Proof. intros; unfold match_prefix; split; intros. - rewrite eqb_spec in H1. rewrite <- H1. symmetry. apply (proj1 (mask_spec _ _ _ H)); auto. - apply eqb_eq; auto. intro n0. elim n0. rewrite <- H0. apply testbit_spec; intros. generalize (mask_spec k _ _ H); intros [HA HB]. generalize (mask_spec p _ _ H); intros [HC HD]. destruct (lt_dec n1 n). + rewrite HA; auto; rewrite HC; auto. + rewrite HB; try lia; rewrite HD; try lia; auto. Qed.
imports: Lia Cdcl.Coqlib