fact: Fixpoint bdepth (pf : ZArithProof) : nat := match pf with | DoneProof => O | RatProof _ p => S (bdepth p) | CutProof _ p => S (bdepth p) | SplitProof _ p1 p2 => S (Nat.max (bdepth p1) (bdepth p2)) | EnumProof _ _ l => S (List.fold_right (fun pf x => Nat.max (bdepth pf) x) O l) | ExProof _ p => S (bdepth p) end.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory