fact: Fixpoint dec_stabalize (max : nat) (Hstable : forall n, n >= max -> iffT (P n) (P (S n))) (Hdec : forall n, n <= max -> dec (P n)) {struct max} : ({ n : nat & (n <= max) * P n }%type + (forall n, P n -> False))%type.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Classes.Morphisms Coq.ZArith.ZArith