proposition: Fact F6 : forall i, (S n < i)%nat -> Canon_plus i alpha (E0_succ beta).
proof: Proof. destruct alpha, beta; unfold lt, Canon_plus in *; simpl in *. intros i H; destruct i. - inversion H. - destruct i. + inversion H. lia. + apply Cor12_3 with (S (S n)); auto. apply L2_6_2; auto. Qed.
imports: hydras(Iterates Simple_LexProd Exp2) hydras(E0 Canon Paths primRec Hprime) Coq(ArithRing Lia) Compat815 Equations(Equations) hydras(primRec)