fact: Definition pred' (n:nat) : {p:nat | n = S p}+{n = 0} := match n return {p:nat | n = S p}+{n = 0} with | O => inright _ (refl_equal 0) | S p => inleft _ (exist (fun p':nat => S p = S p') p (refl_equal (S p))) end.
imports: ZArith List Arith Lia Zwf