fact: Definition pred' (n:nat) : n <> 0 -> nat := match n return n <> 0 -> nat with | O => fun h:0 <> 0 => False_rec nat (h (refl_equal 0)) | S p => fun h:S p <> 0 => p end.
imports: ZArith List Arith Lia Zwf Inverse_Image Extraction