proposition: Lemma F_alpha_positive (alpha : hE0) (n : nat): (0 < F_alpha.F_ alpha n)%N.
proof: Proof. rewrite /F_. apply /ltP ; apply Nat.le_lt_trans with n; [auto with arith| apply F_alpha.F_alpha_gt]. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec Arith) hydras(DecPreOrder) hydras(T1 E0) hydras(primRec) hydras(F_alpha F_omega) gaia_hydras(T1Bridge GCanon GHprime)