fact: Definition well_founded_induction {A:Type}(R:A->A->Prop) (Rwf:forall x:A, Acc R x)(P:A->Type) (F:forall x:A, (forall y:A, R y x -> P y)-> P x)(x:A) : P x := Acc_iter R P F x (Rwf x).
imports: ZArith List Arith Lia Zwf Inverse_Image Extraction