proposition: Theorem match_prefix_spec': forall k p m n, is_mask m n -> mask p m = p -> (match_prefix k p m = false <-> k <> p /\ exists n', (n' < n)%nat /\ testbit (branching_bit k p) n' = true).
proof: Proof. intros; unfold match_prefix; split; intros. - rewrite eqb_false in H1. rename H1 into n0. split. + red; intros. subst k. apply n0; auto. + assert (k <> p) by (red; intros; subst k; apply n0; auto). generalize (branching_bit_spec k p H1). intros [n' [HA [HB HC]]]. exists n'; split; auto. * destruct (lt_dec n' n); auto. generalize (proj2 (match_prefix_spec k _ _ _ H H0)). intros. assert (match_prefix k p m = true). { apply H2. intros; apply HB; lia. } unfold match_prefix in H3. rewrite eqb_spec in H3; congruence. * apply HA; auto. - destruct H1 as [H1 [n' [H2 H3]]]. rewrite eqb_false. intro. generalize (branching_bit_spec _ _ H1). intros [n'' [HA [HB HC]]]. assert (n'' = n') by (apply HA; auto). subst n''. elim HC. eapply (match_prefix_spec k p m n H H0); auto. unfold match_prefix. apply eqb_eq; auto. congruence. Qed.
imports: List Bool ZArith Lia