fact: Fixpoint pred (c:T1) : option T1 := match c with zero => None | cons zero 0 _ => Some zero | cons zero (S n) _ => Some (cons zero n zero) | cons a n b => match (pred b) with None => None | Some c => Some (cons a n c) end end.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List