proposition: Lemma ltof_bdepth_split_r : forall p pf1 pf2, ltof ZArithProof bdepth pf2 (SplitProof p pf1 pf2).
proof: Proof. intros. unfold ltof. simpl. rewrite Nat.lt_succ_r. 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