proposition: Lemma in_bdepth : forall l a b y, In y l -> ltof ZArithProof bdepth y (EnumProof a b l).
proof: Proof. intros l; induction l as [|a l IHl]. - simpl. tauto. - simpl. intros a0 b y H. destruct H as [H|H]. + subst. unfold ltof. simpl. generalize ( (fold_right (fun (pf : ZArithProof) (x : nat) => Nat.max (bdepth pf) x) 0%nat l)). intros. generalize (bdepth y) ; intros. rewrite Nat.lt_succ_r. apply Nat.le_max_l. + generalize (IHl a0 b y H). unfold ltof. simpl. generalize ( (fold_right (fun (pf : ZArithProof) (x : nat) => Nat.max (bdepth pf) x) 0%nat l)). intros. eapply Nat.lt_le_trans. * eassumption. * rewrite <- Nat.succ_le_mono. apply Nat.le_max_r. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory Wf_nat