fact: Definition Acc_inv {A:Type}(R:A->A->Prop)(x:A)(Hacc:Acc R x) : forall y:A, R y x -> Acc R y := match Hacc as H in (Acc _ x) return (forall y:A, R y x -> Acc R y) with | Acc_intro x f => f end.
imports: ZArith List Arith Lia Zwf Inverse_Image Extraction