proposition: Lemma F_alpha_0_eq : forall alpha: E0, F_ alpha 0 = 1.
proof: Proof. intro alpha. pattern alpha; apply well_founded_induction with E0lt. - apply E0lt_wf. - clear alpha; intros alpha Halpha. destruct (Zero_Limit_Succ_dec alpha). destruct s. + subst alpha; now rewrite F_zero_eqn. + rewrite F_lim_eqn;auto; unfold Canon. rewrite Halpha. auto. Search (Canon ?a _ o< ?a). apply (@Canon_lt 0 alpha). intro Heq; subst. discriminate. + destruct s; subst; rewrite F_succ_eqn; simpl; apply Halpha, Lt_Succ. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)