proposition: Lemma QD0 : dominates_from 2 (f_ (E0_succ E0zero)) (f_ E0zero).
proof: Proof. intros p Hp; rewrite f_succ_eqn, f_zero_eqn. apply Nat.lt_le_trans with (iterate S p p). - replace (iterate S p p) with (p + p). + lia. + clear Hp; generalize p at 2 4; induction p. * cbn; reflexivity. * intro p0; cbn; now rewrite IHp. - apply Nat.eq_le_incl, iterate_ext. intros ?; now rewrite f_zero_eqn. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)